1  /-
  2  Copyright (c) 2018 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Mario Carneiro
  5  
  6  The partial recursive functions are defined similarly to the primitive
  7  recursive functions, but now all functions are partial, implemented
  8  using the `roption` monad, and there is an additional operation, called
  9  μ-recursion, which performs unbounded minimization.
 10  -/
 11  import computability.primrec data.pfun
src         └───────────────────┘ └───────┘
 12  
 13  open encodable denumerable roption
 14  
 15  namespace nat
 16  
 17  section rfind
 18  parameter (p : ℕ →. bool)
id                   └┘ └──┘
src                  └┘ └──┘
typ                  └┘ └──┘
doc                   └┘
 19  
 20  private def lbp (m n : ℕ) : Prop := m = n + 1 ∧ ∀ k ≤ n, ff ∈ p k
id                                                    └┘   
src                                                      └┘ 
typ                                                   └┘   
 21  
 22  parameter (H : ∃ n, tt ∈ p n ∧ ∀ k < n, (p k).dom)
id                    └┘                 └─┘
src                    └┘                    └─┘
typ                   └┘                 └─┘
 23  
 24  private def wf_lbp : well_founded lbp :=
id                        └──────────┘ └─┘
src                       └──────────┘ └─┘
typ                       └──────────┘ └─┘
 25  ⟨let ⟨n, pn⟩ := H in begin
id    └─┘            
typ   └─┘            
st                        └─────
 26    suffices : ∀m k, n ≤ k + m → acc (lbp p) k,
id                               └─┘  └─┘ 
src    └─────────┘ └─┘     └─┘ └─┘ └┘
typ    └─────────┘ └─┘    └─┘ └─┘└┘
doc    └─────────┘ └─┘               └┘
txt    └─────────┘ └─┘               └┘
par    └─────────┘ └─┘               └┘
pid    └───────┘└┘ └─┘               └┘
st   ───────────────────────────────────────────┘└─
 27    { from λa, this _ _ (nat.le_add_left _ _) },
id                └──┘      └─────────────┘
src      └───┘ └─┘    └───┘ └─────────────┘└────┘
typ      └───┘ └─┘└──┘└───┘ └─────────────┘└────┘
doc      └───┘ └─┘    └───┘                └────┘
txt      └───┘ └─┘    └───┘                └────┘
par      └───┘ └─┘    └───┘                └────┘
pid      └───┘ └─┘    └───┘                └───┘
st   ───┘└──────────────────────────────────────┘└┘
 28    intros m k kn,
src    └───────────┘
typ    └───────────┘
doc    └───────────┘
txt    └───────────┘
par    └───────────┘
pid          └─────┘
st   ──────────────┘└─
 29    induction m with m IH generalizing k;
id               
src    └────────┘ └───────────────────────┘
typ    └────────┘└───────────────────────┘
doc    └────────┘ └───────────────────────┘
txt    └────────┘ └───────────────────────┘
par    └────────┘ └───────────────────────┘
pid              └───────┘└─────────────┘
st   ────────────────────────────────────────
 30      refine ⟨_, λ y r, _⟩; rcases r with ⟨rfl, a⟩,
id                                    
src      └─────┘ └─┘ └──────┘  └─────┘ └────────────┘
typ      └─────┘ └─┘ └──────┘  └─────┘└────────────┘
doc      └─────┘ └─┘ └──────┘  └─────┘ └────────────┘
txt      └─────┘ └─┘ └──────┘  └─────┘ └────────────┘
par      └─────┘ └─┘ └──────┘  └─────┘ └────────────┘
pid             └─┘ └──────┘         └────────────┘
st   ───────────────────────────────────────────────┘└─
 31    { injection mem_unique pn.1 (a _ kn) },
id                 └────────┘ └┘       └┘
src      └────────┘└────────┘  └─┘  └─┘  └┘
typ      └────────┘└────────┘└┘└─┘ └─┘└┘└┘
doc      └────────┘            └─┘  └─┘  └┘
txt      └────────┘            └─┘  └─┘  └┘
par      └────────┘            └─┘  └─┘  └┘
pid                           └─┘  └─┘  
st   ───┘└─────────────────────────────────┘└┘
 32    { exact IH _ (by rw nat.add_right_comm; exact kn) }
id             └┘          └────────────────┘        └┘
src      └────┘  └─┘   └─┘└────────────────┘└──────┘  └┘
typ      └────┘└┘└─┘   └─┘└────────────────┘└──────┘└┘└┘
doc      └────┘  └─┘   └─┘                  └──────┘  └┘
txt      └────┘  └─┘   └─┘                  └──────┘  └┘
par      └────┘  └─┘   └─┘                  └──────┘  └┘
pid             └─┘   └──┘                  └──────┘  
st   ─────────────────┘└──────────────────────────────┘└┘└─
 33  end⟩
st   ──┘
 34  
 35  def rfind_x : {n // tt ∈ p n ∧ ∀m < n, ff ∈ p m} :=
id                     └┘           └┘   
src                     └┘               └┘ 
typ                    └┘           └┘   
 36  suffices ∀ k, (∀n < k, ff ∈ p n) → {n // tt ∈ p n ∧ ∀m < n, ff ∈ p m},
id                       └┘           └┘           └┘   
src                         └┘              └┘               └┘ 
typ                      └┘           └┘           └┘   
 37  from this 0 (λ n, (nat.not_lt_zero _).elim),
id        └──┘         └─────────────┘   └──┘
src                     └─────────────┘   └──┘
typ       └──┘         └─────────────┘   └──┘
 38  @well_founded.fix _ _ lbp wf_lbp begin
id    └──────────────┘     └─┘ └────┘
src   └──────────────┘     └─┘ └────┘
typ   └──────────────┘     └─┘ └────┘
st                                    └─────
 39    intros m IH al,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid          └──────┘
st   ───────────────┘└─
 40    have pm : (p m).dom,
id                 
src    └────────┘   └───┘
typ    └────────┘ └───┘
doc    └────────┘   └───┘
txt    └────────┘   └───┘
par    └────────┘   └───┘
pid    └─────┘└─┘   └──┘
st   ────────────────────┘└─
 41    { rcases H with ⟨n, h₁, h₂⟩,
id              
src      └─────┘ └───────────────┘
typ      └─────┘└───────────────┘
doc      └─────┘ └───────────────┘
txt      └─────┘ └───────────────┘
par      └─────┘ └───────────────┘
pid             └───────────────┘
st   ───┘└───────────────────────┘└─
 42      rcases decidable.lt_trichotomy m n with h₃|h₃|h₃,
id              └─────────────────────┘  
src      └─────┘└─────────────────────┘  └────────────┘
typ      └─────┘└─────────────────────┘└────────────┘
doc      └─────┘                         └────────────┘
txt      └─────┘                         └────────────┘
par      └─────┘                         └────────────┘
pid                                     └────────────┘
st   ───────────────────────────────────────────────────┘└─
 43      { exact h₂ _ h₃ },
id               └┘   └┘
src        └────┘  └─┘  
typ        └────┘└┘└─┘└┘
doc        └────┘  └─┘  
txt        └────┘  └─┘  
par        └────┘  └─┘  
pid               └─┘  
st   ─────┘└────────────┘└┘
 44      { rw h₃, exact h₁.fst },
id            └┘        └────┘
src        └─┘    └────┘└────┘
typ        └─┘└┘  └────┘└────┘
doc        └─┘    └────┘      
txt        └─┘    └────┘      
par        └─┘    └────┘      
pid                         
st   ─────┘└───┘└─────────────┘└┘
 45      { injection mem_unique h₁ (al _ h₃) } },
id                   └────────┘ └┘  └┘   └┘
src        └────────┘└────────┘     └─┘  └┘
typ        └────────┘└────────┘└┘ └┘└─┘└┘└┘
doc        └────────┘               └─┘  └┘
txt        └────────┘               └─┘  └┘
par        └────────┘               └─┘  └┘
pid                                └─┘  
st   ───────────────────────────────────────┘└──┘
 46    cases e : (p m).get pm,
id                       └┘
src    └────┘ └─┘   └────┘
typ    └────┘ └─┘ └────┘└┘
doc    └────┘ └─┘   └────┘
txt    └────┘ └─┘   └────┘
par    └────┘ └─┘   └────┘
pid          └─┘   └────┘
st   ───────────────────────┘└─
 47    { suffices,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
 48      exact IH _ ⟨rfl, this⟩ (λ n h, this _ (le_of_lt_succ h)),
id             └┘    └─┘                └──┘    └───────────┘
src      └────┘  └─┘ └─┘└┘    └┘  └────┘    └─┘ └───────────┘ └┘
typ      └────┘└┘└─┘ └─┘└┘    └┘  └────┘└──┘└─┘ └───────────┘ └┘
doc      └────┘  └─┘    └┘    └┘  └────┘    └─┘               └┘
txt      └────┘  └─┘    └┘    └┘  └────┘    └─┘               └┘
par      └────┘  └─┘    └┘    └┘  └────┘    └─┘               └┘
pid             └─┘    └┘    └┘  └────┘    └─┘               └┘
st   ───────────────────────────────────────────────────────────┘└─
 49      intros n h, cases decidable.lt_or_eq_of_le h with h h,
id                         └──────────────────────┘ 
src      └────────┘  └────┘└──────────────────────┘ └───────┘
typ      └────────┘  └────┘└──────────────────────┘└───────┘
doc      └────────┘  └────┘                         └───────┘
txt      └────────┘  └────┘                         └───────┘
par      └────────┘  └────┘                         └───────┘
pid            └──┘                                └───────┘
st   ─────────────┘└─────────────────────────────────────────┘└─
 50      { exact al _ h },
id               └┘   
src        └────┘  └─┘ 
typ        └────┘└┘└─┘
doc        └────┘  └─┘ 
txt        └────┘  └─┘ 
par        └────┘  └─┘ 
pid               └─┘ 
st   ─────┘└───────────┘└┘
 51      { rw h, exact ⟨_, e⟩ } },
id                        
src        └─┘   └────┘ └─┘ └┘
typ        └─┘  └────┘ └─┘└┘
doc        └─┘   └────┘ └─┘ └┘
txt        └─┘   └────┘ └─┘ └┘
par        └─┘   └────┘ └─┘ └┘
pid                   └─┘ 
st   ─────────┘└─────────────┘└──┘
 52    { exact ⟨m, ⟨_, e⟩, al⟩ }
id                       └┘
src      └────┘  └┘ └─┘ └─┘  └┘
typ      └────┘ └┘ └─┘└─┘└┘└┘
doc      └────┘  └┘ └─┘ └─┘  └┘
txt      └────┘  └┘ └─┘ └─┘  └┘
par      └────┘  └┘ └─┘ └─┘  └┘
pid             └┘ └─┘ └─┘  
st   ─────────────────────────┘└─
 53  end
st   ──┘
 54  
 55  end rfind
 56  
 57  def rfind (p : ℕ →. bool) : roption ℕ :=
id                   └┘ └──┘    └─────┘ 
src                  └┘ └──┘    └─────┘ 
typ                  └┘ └──┘    └─────┘ 
doc                   └┘         └─────┘
 58  ⟨_, λ h, (rfind_x p h).1⟩
id            └─────┘   
src            └─────┘     
typ           └─────┘   
 59  
 60  theorem rfind_spec {p : ℕ →. bool} {n : ℕ} (h : n ∈ rfind p) : tt ∈ p n :=
id                            └┘ └──┘                └───┘     └┘   
src                           └┘ └──┘                 └───┘      └┘ 
typ                           └┘ └──┘                └───┘     └┘   
doc                            └┘
 61  h.snd ▸ (rfind_x p h.fst).2.1
id   └──┘   └─────┘  └──┘  
src   └──┘   └─────┘    └──┘  
typ  └──┘   └─────┘  └──┘  
 62  
 63  theorem rfind_min {p : ℕ →. bool} {n : ℕ} (h : n ∈ rfind p) :
id                           └┘ └──┘                └───┘ 
src                          └┘ └──┘                 └───┘
typ                          └┘ └──┘                └───┘ 
doc                           └┘
 64    ∀ {m : ℕ}, m < n → ff ∈ p m :=
id                    └┘   
src                     └┘ 
typ                   └┘   
 65  h.snd ▸ (rfind_x p h.fst).2.2
id   └──┘   └─────┘  └──┘  
src   └──┘   └─────┘    └──┘  
typ  └──┘   └─────┘  └──┘  
 66  
 67  @[simp] theorem rfind_dom {p : ℕ →. bool} :
id                                   └┘ └──┘
src                                  └┘ └──┘
typ                                  └┘ └──┘
doc    └──┘                           └┘
 68    (rfind p).dom ↔ ∃ n, tt ∈ p n ∧ ∀ {m : ℕ}, m < n → (p m).dom :=
id      └───┘  └─┘     └┘                       └─┘
src     └───┘   └─┘      └┘                             └─┘
typ     └───┘  └─┘     └┘                       └─┘
 69  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
 70  
 71  @[simp] theorem rfind_dom' {p : ℕ →. bool} :
id                                    └┘ └──┘
src                                   └┘ └──┘
typ                                   └┘ └──┘
doc    └──┘                            └┘
 72    (rfind p).dom ↔ ∃ n, tt ∈ p n ∧ ∀ {m : ℕ}, m ≤ n → (p m).dom :=
id      └───┘  └─┘     └┘                       └─┘
src     └───┘   └─┘      └┘                             └─┘
typ     └───┘  └─┘     └┘                       └─┘
 73  exists_congr $ λ n, and_congr_right $ λ pn,
id   └──────────┘       └─────────────┘     └┘
src  └──────────┘        └─────────────┘
typ  └──────────┘       └─────────────┘     └┘
 74  ⟨λ H m h, (eq_or_lt_of_le h).elim (λ e, e.symm ▸ pn.fst) (H _),
id           └────────────┘  └──┘       └───┘  └┘└──┘   
src             └────────────┘   └──┘         └───┘    └──┘
typ          └────────────┘  └──┘       └───┘  └┘└──┘   
 75   λ H m h, H (le_of_lt h)⟩
id            └──────┘ 
src               └──────┘
typ           └──────┘ 
 76  
 77  @[simp] theorem mem_rfind {p : ℕ →. bool} {n : ℕ} :
id                                   └┘ └──┘       
src                                  └┘ └──┘       
typ                                  └┘ └──┘       
doc    └──┘                           └┘
 78    n ∈ rfind p ↔ tt ∈ p n ∧ ∀ {m : ℕ}, m < n → ff ∈ p m :=
id       └───┘   └┘                    └┘   
src       └───┘    └┘                        └┘ 
typ      └───┘   └┘                    └┘   
 79  ⟨λ h, ⟨rfind_spec h, @rfind_min _ _ h⟩,
id         └────────┘    └───────┘     
src         └────────┘     └───────┘
typ        └────────┘    └───────┘     
 80    λ ⟨h₁, h₂⟩, let ⟨m, hm⟩ := dom_iff_mem.1 $
id       └┘  └┘   └─┘            └─────────┘
src                               └─────────┘
typ      └┘  └┘   └─┘            └─────────┘
 81      (@rfind_dom p).2 ⟨_, h₁, λ m mn, (h₂ mn).fst⟩ in
id         └───────┘               └┘      └┘ └─┘
src        └───────┘                            └─┘
typ        └───────┘               └┘      └┘ └─┘
 82    begin
st     └─────
 83      rcases lt_trichotomy m n with h|h|h,
id              └───────────┘  
src      └─────┘└───────────┘  └─────────┘
typ      └─────┘└───────────┘└─────────┘
doc      └─────┘               └─────────┘
txt      └─────┘               └─────────┘
par      └─────┘               └─────────┘
pid                           └─────────┘
st   ──────────────────────────────────────┘└─
 84      { injection mem_unique (h₂ h) (rfind_spec hm) },
id                   └────────┘  └┘    └────────┘ └┘
src        └────────┘└────────┘    └┘ └────────┘  └┘
typ        └────────┘└────────┘ └┘└┘ └────────┘└┘└┘
doc        └────────┘              └┘             └┘
txt        └────────┘              └┘             └┘
par        └────────┘              └┘             └┘
pid                               └┘             
st   ─────┘└──────────────────────────────────────────┘└┘
 85      { rwa ← h },
id               
src        └────┘ 
typ        └────┘
doc        └────┘ 
txt        └────┘ 
par        └────┘ 
pid           └─┘ 
st   ─────┘└──────┘└┘
 86      { injection mem_unique h₁ (rfind_min hm h) },
id                   └────────┘ └┘  └───────┘ └┘ 
src        └────────┘└────────┘   └───────┘   └┘
typ        └────────┘└────────┘└┘ └───────┘└┘└┘
doc        └────────┘                         └┘
txt        └────────┘                         └┘
par        └────────┘                         └┘
pid                                          
st   ──────────────────────────────────────────────┘└──
 87    end⟩
st   ────┘
 88  
 89  theorem rfind_min' {p : ℕ → bool} {m : ℕ} (pm : p m) :
id                              └──┘                
src                             └──┘       
typ                             └──┘                
 90    ∃ n ∈ rfind p, n ≤ m :=
id         └───┘    
src         └───┘     
typ        └───┘    
 91  have tt ∈ (p : ℕ →. bool) m, from ⟨trivial, pm⟩,
id        └┘       └┘ └──┘          └─────┘  └┘
src       └┘        └┘ └──┘           └─────┘
typ       └┘       └┘ └──┘          └─────┘  └┘
doc                   └┘
 92  let ⟨n, hn⟩ := dom_iff_mem.1 $
id   └─┘    └┘     └─────────┘
src                 └─────────┘
typ  └─┘    └┘     └─────────┘
 93    (@rfind_dom p).2 ⟨m, this, λ k h, ⟨⟩⟩ in
id       └───────┘       └──┘       
src      └───────┘                      
typ      └───────┘       └──┘       
 94  ⟨n, hn, not_lt.1 $ λ h,
id           └────┘      
src          └────┘
typ          └────┘      
 95    by injection mem_unique this (rfind_min hn h)⟩
id                  └────────┘ └──┘  └───────┘ └┘ 
src       └────────┘└────────┘     └───────┘   
typ       └────────┘└────────┘└──┘ └───────┘└┘
doc       └────────┘                           
txt       └────────┘                           
par       └────────┘                           
pid                                           
st       └─────────────────────────────────────────┘
 96  
 97  theorem rfind_zero_none
 98    (p : ℕ →. bool) (p0 : p 0 = none) : rfind p = none :=
id           └┘ └──┘            └──┘    └───┘   └──┘
src          └┘ └──┘             └──┘    └───┘    └──┘
typ          └┘ └──┘            └──┘    └───┘   └──┘
doc           └┘                   └──┘              └──┘
 99  eq_none_iff.2 $ λ a h,
id   └─────────┘       
src  └─────────┘
typ  └─────────┘       
100  let ⟨n, h₁, h₂⟩ := rfind_dom'.1 h.fst in
id   └─┘         └┘     └────────┘  └──┘
src                     └────────┘   └──┘
typ  └─┘         └┘     └────────┘  └──┘
101  (p0 ▸ h₂ (zero_le _) : (@roption.none bool).dom)
id    └┘      └─────┘        └──────────┘ └──┘ └─┘
src           └─────┘        └──────────┘ └──┘ └─┘
typ   └┘      └─────┘        └──────────┘ └──┘ └─┘
doc                           └──────────┘
102  
103  def rfind_opt {α} (f : ℕ → option α) : roption α :=
id                             └────┘     └─────┘ 
src                            └────┘      └─────┘
typ                            └────┘     └─────┘ 
doc                                         └─────┘
104  (rfind (λ n, (f n).is_some)).bind (λ n, f n)
id    └───┘         └─────┘   └──┘        
src   └───┘            └─────┘   └──┘
typ   └───┘         └─────┘   └──┘        
doc                              └──┘
105  
106  theorem rfind_opt_spec {α} {f : ℕ → option α} {a}
id                                      └────┘ 
src                                     └────┘
typ                                     └────┘ 
107   (h : a ∈ rfind_opt f) : ∃ n, a ∈ f n :=
id           └───────┘          
src           └───────┘           
typ          └───────┘          
108  let ⟨n, h₁, h₂⟩ := mem_bind_iff.1 h in ⟨n, mem_coe.1 h₂⟩
id   └─┘        └┘     └──────────┘          └─────┘
src                     └──────────┘           └─────┘
typ  └─┘        └┘     └──────────┘          └─────┘
109  
110  theorem rfind_opt_dom {α} {f : ℕ → option α} :
id                                     └────┘ 
src                                    └────┘
typ                                    └────┘ 
111    (rfind_opt f).dom ↔ ∃ n a, a ∈ f n :=
id      └───────┘  └─┘         
src     └───────┘   └─┘          
typ     └───────┘  └─┘         
112  ⟨λ h, (rfind_opt_spec ⟨h, rfl⟩).imp (λ n h, ⟨_, h⟩),
id         └────────────┘    └─┘  └─┘            
src         └────────────┘     └─┘  └─┘
typ        └────────────┘    └─┘  └─┘            
113   λ h, begin
id      
typ     
st         └─────
114    have h' : ∃ n, (f n).is_some :=
id                   
src    └────────┘└┘   └────────────
typ    └────────┘└┘  └────────────
doc    └────────┘ └┘    └────────────
txt    └────────┘ └┘    └────────────
par    └────────┘ └┘    └────────────
pid    └─────┘└─┘ └┘    └──────┘└────
st   ──────────────────────────────────
115      h.imp (λ n, option.is_some_iff_exists.2),
id       └───┘       └───────────────────────┘
src  ───┘└───┘  └──┘└───────────────────────┘└─┘
typ  ───┘└───┘  └──┘└───────────────────────┘└─┘
doc  ───┘       └──┘                         └─┘
txt  ───┘       └──┘                         └─┘
par  ───┘       └──┘                         └─┘
pid  ───┘       └──┘                         └─┘
st   ───────────────────────────────────────────┘└─
116    have s := nat.find_spec h',
id               └───────────┘ └┘
src    └────────┘└───────────┘
typ    └────────┘└───────────┘└┘
doc    └────────┘             
txt    └────────┘             
par    └────────┘             
pid    └────┘└─┘             
st   ───────────────────────────┘└─
117    have fd : (rfind (λ n, (f n).is_some)).dom :=
id                └───┘        
src    └────────┘ └───┘  └──┘   └──────────────────
typ    └────────┘ └───┘  └──┘  └──────────────────
doc    └────────┘        └──┘   └──────────────────
txt    └────────┘        └──┘   └──────────────────
par    └────────┘        └──┘   └──────────────────
pid    └─────┘└─┘        └──┘   └────────────┘└────
st   ────────────────────────────────────────────────
118      ⟨nat.find h', by simpa using s.symm, λ _ _, trivial⟩,
id        └──────┘ └┘                 └────┘         └─────┘
src  ───┘ └──────┘  └┘  └──────────┘└────┘└┘ └────┘└─────┘
typ  ───┘ └──────┘└┘└┘  └──────────┘└────┘└┘ └────┘└─────┘
doc  ───┘           └┘  └──────────┘      └┘ └────┘       
txt  ───┘           └┘  └──────────┘      └┘ └────┘       
par  ───┘           └┘  └──────────┘      └┘ └────┘       
pid  ───┘           └┘  └───────────┘      └┘ └────┘       
st   ───────────────────┘└─────────────────┘└───────────────┘└─
119    refine ⟨fd, _⟩,
id             └┘
src    └─────┘   └──┘
typ    └─────┘ └┘└──┘
doc    └─────┘   └──┘
txt    └─────┘   └──┘
par    └─────┘   └──┘
pid             └──┘
st   ───────────────┘└─
120    have := rfind_spec (get_mem fd),
id             └────────┘  └─────┘ └┘
src    └──────┘└────────┘ └─────┘  
typ    └──────┘└────────┘ └─────┘└┘
doc    └──────┘                    
txt    └──────┘                    
par    └──────┘                    
pid    └───┘└─┘                    
st   ────────────────────────────────┘└─
121    simp at this ⊢,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid        └───────┘
st   ───────────────┘└─
122    cases option.is_some_iff_exists.1 this.symm with a e,
id           └───────────────────────┘   └───────┘
src    └────┘└───────────────────────┘└─┘└───────┘└───────┘
typ    └────┘└───────────────────────┘└─┘└───────┘└───────┘
doc    └────┘                         └─┘         └───────┘
txt    └────┘                         └─┘         └───────┘
par    └────┘                         └─┘         └───────┘
pid                                  └─┘         └───────┘
st   ─────────────────────────────────────────────────────┘└─
123    rw e, trivial
id        
src    └─┘   └──────┘
typ    └─┘  └──────┘
doc    └─┘   └──────┘
txt    └─┘   └──────┘
par    └─┘   └──────┘
pid                
st   ─────┘└────────┘
124  end⟩
st   └─┘
125  
126  theorem rfind_opt_mono {α} {f : ℕ → option α}
id                                      └────┘ 
src                                     └────┘
typ                                     └────┘ 
127    (H : ∀ {a m n}, m ≤ n → a ∈ f m → a ∈ f n)
id                                
src                                      
typ                               
128    {a} : a ∈ rfind_opt f ↔ ∃ n, a ∈ f n :=
id             └───────┘        
src             └───────┘         
typ            └───────┘        
129  ⟨rfind_opt_spec, λ ⟨n, h⟩, begin
id    └────────────┘    
src   └────────────┘
typ   └────────────┘    
st                              └─────
130    have h' := rfind_opt_dom.2 ⟨_, _, h⟩,
id                └───────────┘          
src    └─────────┘└───────────┘└─┘ └────┘ 
typ    └─────────┘└───────────┘└─┘ └────┘
doc    └─────────┘             └─┘ └────┘ 
txt    └─────────┘             └─┘ └────┘ 
par    └─────────┘             └─┘ └────┘ 
pid    └─────┘└─┘             └─┘ └────┘ 
st   ─────────────────────────────────────┘└─
131    cases rfind_opt_spec ⟨h', rfl⟩ with k hk,
id           └────────────┘  └┘  └─┘
src    └────┘└────────────┘   └┘└─┘└─────────┘
typ    └────┘└────────────┘ └┘└┘└─┘└─────────┘
doc    └────┘                 └┘   └─────────┘
txt    └────┘                 └┘   └─────────┘
par    └────┘                 └┘   └─────────┘
pid                          └┘   └────────┘
st   ─────────────────────────────────────────┘└─
132    have := (H (le_max_left _ _) h).symm.trans
id                 └─────────┘      
src    └──────┘   └─────────┘└────┘ └────────────
typ    └──────┘   └─────────┘└────┘└────────────
doc    └──────┘              └────┘ └────────────
txt    └──────┘              └────┘ └────────────
par    └──────┘              └────┘ └────────────
pid    └───┘└─┘              └────┘ └────────────
st   ─────────────────────────────────────────────
133            (H (le_max_right _ _) hk),
id                └──────────┘      └┘
src  ─────────┘   └──────────┘└────┘  
typ  ─────────┘  └──────────┘└────┘└┘
doc  ─────────┘               └────┘  
txt  ─────────┘               └────┘  
par  ─────────┘               └────┘  
pid  ─────────┘               └────┘  
st   ──────────────────────────────────┘└─
134    simp at this, simp [this, get_mem]
id                         └──┘  └─────┘
src    └──────────┘  └────┘    └┘└─────┘└┘
typ    └──────────┘  └────┘└──┘└┘└─────┘└┘
doc    └──────────┘  └────┘    └┘       └┘
txt    └──────────┘  └────┘    └┘       └┘
par    └──────────┘  └────┘    └┘       └┘
pid        └─────┘          └┘       
st   ─────────────┘└─────────────────────┘
135  end⟩
st   └─┘
136  
137  inductive partrec : (ℕ →. ℕ) → Prop
id                         └┘ 
src                        └┘ 
typ                        └┘ 
doc                         └┘
138  | zero : partrec (pure 0)
id                     └──┘
src                    └──┘
typ                    └──┘
139  | succ : partrec succ
id                    └──┘
src                   └──┘
typ                   └──┘
140  | left : partrec (λ n, n.unpair.1)
id                         └─────┘
src                          └─────┘
typ                        └─────┘
doc                          └─────┘
141  | right : partrec (λ n, n.unpair.2)
id                          └─────┘
src                           └─────┘
typ                         └─────┘
doc                           └─────┘
142  | pair {f g} : partrec f → partrec g → partrec (λ n, mkpair <$> f n <*> g n)
id                └─────┘    └─────┘                 └────┘ └─┘   └─┘  
src                                                       └────┘ └─┘     └─┘
typ               └─────┘    └─────┘                 └────┘ └─┘   └─┘  
doc                                                       └────┘
143  | comp {f g} : partrec f → partrec g → partrec (λ n, g n >>= f)
id                └─────┘    └─────┘                   └─┘ 
src                                                           └─┘
typ               └─────┘    └─────┘                   └─┘ 
144  | prec {f g} : partrec f → partrec g → partrec (unpaired (λ a n,
id                └─────┘    └─────┘             └──────┘     
src                                                  └──────┘
typ               └─────┘    └─────┘             └──────┘     
145      n.elim (f a) (λ y IH, do i ← IH, g (mkpair a (mkpair y i)))))
id       └───┘         └┘        └┘    └────┘   └────┘  
src       └───┘                              └────┘    └────┘
typ      └───┘         └┘        └┘    └────┘   └────┘  
doc                                          └────┘    └────┘
146  | rfind {f} : partrec f → partrec (λ a,
id                └─────┘               
typ               └─────┘               
147      rfind (λ n, (λ m, m = 0) <$> f (mkpair a n)))
id       └───┘                └─┘   └────┘  
src      └───┘                   └─┘    └────┘
typ      └───┘                └─┘   └────┘  
doc                                      └────┘
148  
149  namespace partrec
150  
151  theorem of_eq {f g : ℕ →. ℕ} (hf : partrec f) (H : ∀ n, f n = g n) : partrec g :=
id                         └┘         └─────┘                    └─────┘ 
src                        └┘         └─────┘                          └─────┘
typ                        └┘         └─────┘                    └─────┘ 
doc                         └┘
152  (funext H : f = g) ▸ hf
id    └────┘         └┘
src   └────┘           
typ   └────┘         └┘
153  
154  theorem of_eq_tot {f : ℕ →. ℕ} {g : ℕ → ℕ}
id                           └┘           
src                          └┘           
typ                          └┘           
doc                           └┘
155    (hf : partrec f) (H : ∀ n, g n ∈ f n) : partrec g :=
id           └─────┘                    └─────┘ 
src          └─────┘                          └─────┘
typ          └─────┘                    └─────┘ 
156  hf.of_eq (λ n, eq_some_iff.2 (H n))
id   └┘└────┘      └─────────┘    
src    └────┘       └─────────┘
typ  └┘└────┘      └─────────┘    
157  
158  theorem of_primrec {f : ℕ → ℕ} (hf : primrec f) : partrec f :=
id                                      └─────┘     └─────┘ 
src                                     └─────┘      └─────┘
typ                                     └─────┘     └─────┘ 
doc                                       └─────┘
159  begin
st   └─────
160    induction hf,
id               └┘
src    └────────┘
typ    └────────┘└┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ─────────────┘└─
161    case nat.primrec.zero { exact zero },
id                                   └──┘
src    └──────────────────────┘└────┘└──┘
typ    └──────────────────────┘└────┘└──┘
doc    └──────────────────────┘└────┘    
txt    └──────────────────────┘└────┘    
par    └──────────────────────┘└────┘    
pid        └───────────────┘└──────┘    └┘
st   ────────────────────────┘└──────────┘└┘
162    case nat.primrec.succ { exact succ },
id                                   └──┘
src    └──────────────────────┘└────┘└──┘
typ    └──────────────────────┘└────┘└──┘
doc    └──────────────────────┘└────┘    
txt    └──────────────────────┘└────┘    
par    └──────────────────────┘└────┘    
pid        └───────────────┘└──────┘    └┘
st   ────────────────────────┘└──────────┘└┘
163    case nat.primrec.left { exact left },
id                                   └──┘
src    └──────────────────────┘└────┘└──┘
typ    └──────────────────────┘└────┘└──┘
doc    └──────────────────────┘└────┘    
txt    └──────────────────────┘└────┘    
par    └──────────────────────┘└────┘    
pid        └───────────────┘└──────┘    └┘
st   ────────────────────────┘└──────────┘└┘
164    case nat.primrec.right { exact right },
id                                    └───┘
src    └───────────────────────┘└────┘└───┘
typ    └───────────────────────┘└────┘└───┘
doc    └───────────────────────┘└────┘     
txt    └───────────────────────┘└────┘     
par    └───────────────────────┘└────┘     
pid        └────────────────┘└──────┘     └┘
st   ─────────────────────────┘└───────────┘└┘
165    case nat.primrec.pair : f g hf hg pf pg {
src    └─────────────────────────────────────────
typ    └─────────────────────────────────────────
doc    └─────────────────────────────────────────
txt    └─────────────────────────────────────────
par    └─────────────────────────────────────────
pid        └───────────────┘└────────────────┘└──
st   ──────────────────────────────────────────┘
166      refine (pf.pair pg).of_eq_tot (λ n, _),
id               └─────┘ └┘
src  ───┘└─────┘ └─────┘  └──────────┘  └────┘└─
typ  ───┘└─────┘ └─────┘└┘└──────────┘  └────┘└─
doc  ───┘└─────┘          └──────────┘  └────┘└─
txt  ───┘└─────┘          └──────────┘  └────┘└─
par  ───┘└─────┘          └──────────┘  └────┘└─
pid  ──────────┘          └──────────┘  └───────
st   ─────────────────────────────────────────┘└─
167      simp [has_seq.seq] },
src  ───┘└────┘           └┘
typ  ───┘└────┘           └┘
doc  ───┘└────┘           └┘
txt  ───┘└────┘           └┘
par  ───┘└────┘           └┘
pid  ─────────┘           └─┘
st   ──────────────────────┘└┘
168    case nat.primrec.comp : f g hf hg pf pg {
src    └─────────────────────────────────────────
typ    └─────────────────────────────────────────
doc    └─────────────────────────────────────────
txt    └─────────────────────────────────────────
par    └─────────────────────────────────────────
pid        └───────────────┘└────────────────┘└──
st   ──────────────────────────────────────────┘
169      refine (pf.comp pg).of_eq_tot (λ n, _),
id               └─────┘ └┘
src  ───┘└─────┘ └─────┘  └──────────┘  └────┘└─
typ  ───┘└─────┘ └─────┘└┘└──────────┘  └────┘└─
doc  ───┘└─────┘          └──────────┘  └────┘└─
txt  ───┘└─────┘          └──────────┘  └────┘└─
par  ───┘└─────┘          └──────────┘  └────┘└─
pid  ──────────┘          └──────────┘  └───────
st   ─────────────────────────────────────────┘└─
170      simp },
src  ───┘└───┘
typ  ───┘└───┘
doc  ───┘└───┘
txt  ───┘└───┘
par  ───┘└───┘
pid  ─────────┘
st   ────────┘└┘
171    case nat.primrec.prec : f g hf hg pf pg {
src    └─────────────────────────────────────────
typ    └─────────────────────────────────────────
doc    └─────────────────────────────────────────
txt    └─────────────────────────────────────────
par    └─────────────────────────────────────────
pid        └───────────────┘└────────────────┘└──
st   ──────────────────────────────────────────┘
172      refine (pf.prec pg).of_eq_tot (λ n, _),
id               └─────┘ └┘
src  ───┘└─────┘ └─────┘  └──────────┘  └────┘└─
typ  ───┘└─────┘ └─────┘└┘└──────────┘  └────┘└─
doc  ───┘└─────┘          └──────────┘  └────┘└─
txt  ───┘└─────┘          └──────────┘  └────┘└─
par  ───┘└─────┘          └──────────┘  └────┘└─
pid  ──────────┘          └──────────┘  └───────
st   ─────────────────────────────────────────┘└─
173      simp,
src  ───┘└──┘└─
typ  ───┘└──┘└─
doc  ───┘└──┘└─
txt  ───┘└──┘└─
par  ───┘└──┘└─
pid  ──────────
st   ───────┘└─
174      induction n.unpair.2 with m IH, {simp},
id                 └──────┘
src  ───┘└────────┘└──────┘└──────────┘└─┘└──┘└──
typ  ───┘└────────┘└──────┘└──────────┘└─┘└──┘└──
doc  ───┘└────────┘└──────┘└──────────┘└─┘└──┘└──
txt  ───┘└────────┘        └──────────┘└─┘└──┘└──
par  ───┘└────────┘        └──────────┘└─┘└──┘└──
pid  ─────────────┘        └─────────────────────
st   ─────────────────────────────────┘└─────┘└─
175      simp, exact ⟨_, IH, rfl⟩ },
id                       └┘  └─┘
src  ───┘└──┘└┘└────┘ └─┘  └┘└─┘└┘
typ  ───┘└──┘└┘└────┘ └─┘└┘└┘└─┘└┘
doc  ───┘└──┘└┘└────┘ └─┘  └┘   └┘
txt  ───┘└──┘└┘└────┘ └─┘  └┘   └┘
par  ───┘└──┘└┘└────┘ └─┘  └┘   └┘
pid  ───────────────┘ └─┘  └┘   └─┘
st   ───────┘└───────────────────┘└──
176  end
st   ──┘
177  
178  protected theorem some : partrec some := of_primrec primrec.id
id                            └─────┘ └──┘    └────────┘ └────────┘
src                           └─────┘ └──┘    └────────┘ └────────┘
typ                           └─────┘ └──┘    └────────┘ └────────┘
doc                                   └──┘
179  
180  theorem none : partrec (λ n, none) :=
id                  └─────┘      └──┘
src                 └─────┘       └──┘
typ                 └─────┘      └──┘
doc                               └──┘
181  (of_primrec (nat.primrec.const 1)).rfind.of_eq $
id    └────────┘  └───────────────┘    └───┘ └───┘
src   └────────┘  └───────────────┘    └───┘ └───┘
typ   └────────┘  └───────────────┘    └───┘ └───┘
182  λ n, eq_none_iff.2 $ λ a ⟨h, e⟩, by simpa using h
id       └─────────┘                             
src       └─────────┘                   └──────────┘ 
typ      └─────────┘                 └──────────┘
doc                                      └──────────┘ 
txt                                      └──────────┘ 
par                                      └──────────┘ 
pid                                           └────┘ 
st                                      └──────────────
183  
src  
typ  
doc  
txt  
par  
pid  
st   
184  theorem prec' {f g h}
185    (hf : partrec f) (hg : partrec g) (hh : partrec h) :
id           └─────┘         └─────┘         └─────┘ 
src          └─────┘          └─────┘          └─────┘
typ          └─────┘         └─────┘         └─────┘ 
186    partrec (λ a, (f a).bind (λ n, n.elim (g a)
id     └─────┘         └──┘       └───┘   
src    └─────┘            └──┘         └───┘
typ    └─────┘         └──┘       └───┘   
doc                       └──┘
187      (λ y IH, do i ← IH, h (mkpair a (mkpair y i))))) :=
id           └┘        └┘    └────┘   └────┘  
src                             └────┘    └────┘
typ          └┘        └┘    └────┘   └────┘  
doc                             └────┘    └────┘
188  ((prec hg hh).comp (pair partrec.some hf)).of_eq $
id     └──┘ └┘ └┘ └──┘   └──┘ └──────────┘ └┘  └───┘
src    └──┘       └──┘   └──┘ └──────────┘     └───┘
typ    └──┘ └┘ └┘ └──┘   └──┘ └──────────┘ └┘  └───┘
189  λ a, ext $ λ s, by simp [(<*>)]; exact
id       └─┘     
src       └─┘           └────┘ └───┘  └────┘
typ      └─┘          └────┘ └───┘  └────┘
doc       └─┘           └────┘ └───┘  └────┘
txt                     └────┘ └───┘  └────┘
par                     └────┘ └───┘  └────┘
pid                          └───┘       
st                     └────────────────────
190  ⟨λ ⟨n, h₁, h₂⟩, ⟨_, ⟨_, h₁, rfl⟩, by simpa using h₂⟩,
src    └┘ └┘  └┘  └─┘ └─┘ └─┘  └┘   └─┘  └──────────┘  └──
typ    └┘ └┘  └┘  └─┘ └─┘ └─┘  └┘   └─┘  └──────────┘  └──
doc    └┘ └┘  └┘  └─┘ └─┘ └─┘  └┘   └─┘  └──────────┘  └──
txt    └┘ └┘  └┘  └─┘ └─┘ └─┘  └┘   └─┘  └──────────┘  └──
par    └┘ └┘  └┘  └─┘ └─┘ └─┘  └┘   └─┘  └──────────┘  └──
pid    └┘ └┘  └┘  └─┘ └─┘ └─┘  └┘   └─┘  └───────────┘  └──
st   ───────────────────────────────────┘               └──
191   λ ⟨_, ⟨n, h₁, rfl⟩, h₂⟩, ⟨_, h₁, by simpa using h₂⟩⟩
src   └───┘  └┘  └┘   └─┘  └─┘ └─┘  └┘  └──────────┘  └──
typ   └───┘  └┘  └┘   └─┘  └─┘ └─┘  └┘  └──────────┘  └──
doc   └───┘  └┘  └┘   └─┘  └─┘ └─┘  └┘  └──────────┘  └──
txt   └───┘  └┘  └┘   └─┘  └─┘ └─┘  └┘  └──────────┘  └──
par   └───┘  └┘  └┘   └─┘  └─┘ └─┘  └┘  └──────────┘  └──
pid   └───┘  └┘  └┘   └─┘  └─┘ └─┘  └┘  └───────────┘  └┘
st   ───────────────────────────────────┘               └──
192  
src  
typ  
doc  
txt  
par  
pid  
st   
193  theorem ppred : partrec (λ n, ppred n) :=
id                   └─────┘      └───┘ 
src                  └─────┘       └───┘
typ                  └─────┘      └───┘ 
doc                                └───┘
194  have primrec₂ (λ n m, if n = nat.succ m then 0 else 1),
id        └──────┘            └──────┘ 
src       └──────┘               └──────┘
typ       └──────┘            └──────┘ 
doc       └──────┘
195  from (primrec.ite
id         └─────────┘
src        └─────────┘
typ        └─────────┘
196    (@@primrec_rel.comp _ _ _ _ _ _ _ primrec.eq
id        └──────────────┘               └────────┘
src       └──────────────┘               └────────┘
typ       └──────────────┘               └────────┘
197      primrec.fst
id       └─────────┘
src      └─────────┘
typ      └─────────┘
198      (_root_.primrec.succ.comp primrec.snd))
id        └─────────────────┘└───┘ └─────────┘
src       └─────────────────┘└───┘ └─────────┘
typ       └─────────────────┘└───┘ └─────────┘
199    (_root_.primrec.const 0) (_root_.primrec.const 1)).to₂,
id      └──────────────────┘     └──────────────────┘    └─┘
src     └──────────────────┘     └──────────────────┘    └─┘
typ     └──────────────────┘     └──────────────────┘    └─┘
200  (of_primrec (primrec₂.unpaired'.2 this)).rfind.of_eq $
id    └────────┘  └────────────────┘  └──┘  └───┘ └───┘
src   └────────┘  └────────────────┘        └───┘ └───┘
typ   └────────┘  └────────────────┘  └──┘  └───┘ └───┘
201  λ n, begin
id     
typ    
st        └─────
202    cases n; simp,
id           
src    └────┘   └──┘
typ    └────┘  └──┘
doc    └────┘   └──┘
txt    └────┘   └──┘
par    └────┘   └──┘
pid         
st   ──────────────┘└─
203    { exact eq_none_iff.2 (λ a ⟨⟨m, h, _⟩, _⟩,
id             └─────────┘
src      └────┘└─────────┘└─┘  └──┘  └┘ └─────────
typ      └────┘└─────────┘└─┘  └──┘  └┘ └─────────
doc      └────┘           └─┘  └──┘  └┘ └─────────
txt      └────┘           └─┘  └──┘  └┘ └─────────
par      └────┘           └─┘  └──┘  └┘ └─────────
pid                      └─┘  └──┘  └┘ └─────────
st   ───┘└────────────────────────────────────────
204        by simpa [show 0 ≠ m.succ, by intro h; injection h] using h) },
id                           └────┘                                
src  ─────┘  └─────┘    └─┘└────┘└───┘└─────┘└┘└────────┘ └──────┘ └┘
typ  ─────┘  └─────┘    └─┘└────┘└───┘└─────┘└┘└────────┘└──────┘└┘
doc  ─────┘  └─────┘    └─┘       └───┘└─────┘└┘└────────┘ └──────┘ └┘
txt  ─────┘  └─────┘    └─┘       └───┘└─────┘└┘└────────┘ └──────┘ └┘
par  ─────┘  └─────┘    └─┘       └───┘└─────┘└┘└────────┘ └──────┘ └┘
pid  ─────┘  └──────┘    └─┘       └──────────────────────┘ └──────┘ 
st   ───────┘└─────────────────────────┘└───────────────────┘└───────┘└┘└┘
205    { refine eq_some_iff.2 _,
id              └─────────┘
src      └─────┘└─────────┘└──┘
typ      └─────┘└─────────┘└──┘
doc      └─────┘           └──┘
txt      └─────┘           └──┘
par      └─────┘           └──┘
pid                       └──┘
st   ─────────────────────────┘└─
206      simp, intros m h, simp [ne_of_gt h] }
id                               └──────┘ 
src      └──┘  └────────┘  └────┘└──────┘ └┘
typ      └──┘  └────────┘  └────┘└──────┘└┘
doc      └──┘  └────────┘  └────┘         └┘
txt      └──┘  └────────┘  └────┘         └┘
par      └──┘  └────────┘  └────┘         └┘
pid                  └──┘               
st   ───────┘└──────────┘└──────────────────┘└─
207  end
st   ──┘
208  
209  end partrec
210  
211  end nat
212  
213  def partrec {α σ} [primcodable α] [primcodable σ]
id                      └─────────┘    └─────────┘ 
src                     └─────────┘     └─────────┘
typ                     └─────────┘    └─────────┘ 
doc                     └─────────┘     └─────────┘
214    (f : α →. σ) := nat.partrec (λ n,
id           └┘      └─────────┘    
src           └┘       └─────────┘
typ          └┘      └─────────┘    
doc           └┘
215    roption.bind (decode α n) (λ a, (f a).map encode))
id     └──────────┘  └────┘            └─┘  └────┘
src    └──────────┘  └────┘                 └─┘  └────┘
typ    └──────────┘  └────┘            └─┘  └────┘
doc    └──────────┘                         └─┘
216  
217  def partrec₂ {α β σ} [primcodable α] [primcodable β] [primcodable σ]
id                         └─────────┘    └─────────┘    └─────────┘ 
src                        └─────────┘     └─────────┘     └─────────┘
typ                        └─────────┘    └─────────┘    └─────────┘ 
doc                        └─────────┘     └─────────┘     └─────────┘
218    (f : α → β →. σ) := partrec (λ p : α × β, f p.1 p.2)
id              └┘      └─────┘               
src               └┘       └─────┘                    
typ             └┘      └─────┘               
doc               └┘
219  
220  def computable {α σ} [primcodable α] [primcodable σ] (f : α → σ) := partrec (f : α →. σ)
id                         └─────────┘    └─────────┘                └─────┘      └┘ 
src                        └─────────┘     └─────────┘                   └─────┘        └┘
typ                        └─────────┘    └─────────┘                └─────┘      └┘ 
doc                        └─────────┘     └─────────┘                                  └┘
221  
222  def computable₂ {α β σ} [primcodable α] [primcodable β] [primcodable σ]
id                            └─────────┘    └─────────┘    └─────────┘ 
src                           └─────────┘     └─────────┘     └─────────┘
typ                           └─────────┘    └─────────┘    └─────────┘ 
doc                           └─────────┘     └─────────┘     └─────────┘
223    (f : α → β → σ) := computable (λ p : α × β, f p.1 p.2)
id                     └────────┘               
src                       └────────┘                    
typ                    └────────┘               
224  
225  theorem primrec.to_comp {α σ} [primcodable α] [primcodable σ]
id                                  └─────────┘    └─────────┘ 
src                                 └─────────┘     └─────────┘
typ                                 └─────────┘    └─────────┘ 
doc                                 └─────────┘     └─────────┘
226    {f : α → σ} (hf : primrec f) : computable f :=
id                     └─────┘     └────────┘ 
src                      └─────┘      └────────┘
typ                    └─────┘     └────────┘ 
doc                      └─────┘
227  (nat.partrec.ppred.comp (nat.partrec.of_primrec hf)).of_eq $
id    └───────────────┘└───┘  └────────────────────┘ └┘  └───┘
src   └───────────────┘└───┘  └────────────────────┘     └───┘
typ   └───────────────┘└───┘  └────────────────────┘ └┘  └───┘
228  λ n, by simp; cases decode α n; simp
id                      └────┘  
src          └──┘  └────┘└────┘    └────
typ         └──┘  └────┘└────┘  └────
doc          └──┘  └────┘          └────
txt          └──┘  └────┘          └────
par          └──┘  └────┘          └────
pid                                   
st          └─────────────────────────────
229  
src  
typ  
doc  
txt  
par  
pid  
st   
230  theorem primrec₂.to_comp {α β σ} [primcodable α] [primcodable β] [primcodable σ]
id                                     └─────────┘    └─────────┘    └─────────┘ 
src                                    └─────────┘     └─────────┘     └─────────┘
typ                                    └─────────┘    └─────────┘    └─────────┘ 
doc                                    └─────────┘     └─────────┘     └─────────┘
231    {f : α → β → σ} (hf : primrec₂ f) : computable₂ f := hf.to_comp
id                        └──────┘     └─────────┘     └┘└──────┘
src                          └──────┘      └─────────┘        └──────┘
typ                       └──────┘     └─────────┘     └┘└──────┘
doc                          └──────┘
232  
233  theorem computable.part {α σ} [primcodable α] [primcodable σ]
id                                  └─────────┘    └─────────┘ 
src                                 └─────────┘     └─────────┘
typ                                 └─────────┘    └─────────┘ 
doc                                 └─────────┘     └─────────┘
234    {f : α → σ} (hf : computable f) : partrec (f : α →. σ) := hf
id                     └────────┘     └─────┘      └┘      └┘
src                      └────────┘      └─────┘        └┘
typ                    └────────┘     └─────┘      └┘      └┘
doc                                                     └┘
235  
236  theorem computable₂.part {α β σ} [primcodable α] [primcodable β] [primcodable σ]
id                                     └─────────┘    └─────────┘    └─────────┘ 
src                                    └─────────┘     └─────────┘     └─────────┘
typ                                    └─────────┘    └─────────┘    └─────────┘ 
doc                                    └─────────┘     └─────────┘     └─────────┘
237    {f : α → β → σ} (hf : computable₂ f) : partrec₂ (λ a, (f a : β →. σ)) := hf
id                        └─────────┘     └──────┘            └┘       └┘
src                          └─────────┘      └──────┘                └┘
typ                       └─────────┘     └──────┘            └┘       └┘
doc                                                                   └┘
238  
239  namespace computable
240  variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
241  variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id              └─────────┘     └─────────┘     └─────────┘     └─────────┘
src             └─────────┘     └─────────┘     └─────────┘     └─────────┘
typ             └─────────┘     └─────────┘     └─────────┘     └─────────┘
doc             └─────────┘     └─────────┘     └─────────┘     └─────────┘
242  
243  theorem of_eq {f g : α → σ} (hf : computable f) (H : ∀ n, f n = g n) : computable g :=
id                                   └────────┘                    └────────┘ 
src                                    └────────┘                          └────────┘
typ                                  └────────┘                    └────────┘ 
244  (funext H : f = g) ▸ hf
id    └────┘         └┘
src   └────┘           
typ   └────┘         └┘
245  
246  theorem const (s : σ) : computable (λ a : α, s) :=
id                          └────────┘          
src                          └────────┘
typ                         └────────┘          
247  (primrec.const _).to_comp
id    └───────────┘   └─────┘
src   └───────────┘   └─────┘
typ   └───────────┘   └─────┘
248  
249  theorem of_option {f : α → option β}
id                             └────┘ 
src                             └────┘
typ                            └────┘ 
250    (hf : computable f) : partrec (λ a, (f a : roption β)) :=
id           └────────┘     └─────┘           └─────┘ 
src          └────────┘      └─────┘              └─────┘
typ          └────────┘     └─────┘           └─────┘ 
doc                                               └─────┘
251  (nat.partrec.ppred.comp hf).of_eq $ λ n, begin
id    └───────────────┘└───┘ └┘ └───┘      
src   └───────────────┘└───┘    └───┘
typ   └───────────────┘└───┘ └┘ └───┘      
st                                            └─────
252    cases decode α n with a; simp,
id           └────┘  
src    └────┘└────┘  └─────┘  └──┘
typ    └────┘└────┘└─────┘  └──┘
doc    └────┘        └─────┘  └──┘
txt    └────┘        └─────┘  └──┘
par    └────┘        └─────┘  └──┘
pid                 └─────┘
st   ──────────────────────────────┘└─
253    cases f a with b; simp
id            
src    └────┘  └─────┘  └───┘
typ    └────┘└─────┘  └───┘
doc    └────┘  └─────┘  └───┘
txt    └────┘  └─────┘  └───┘
par    └────┘  └─────┘  └───┘
pid           └─────┘      
st   ────────────────────────┘
254  end
st   └─┘
255  
256  theorem to₂ {f : α × β → σ} (hf : computable f) : computable₂ (λ a b, f (a, b)) :=
id                                 └────────┘     └─────────┘          
src                                   └────────┘      └─────────┘           
typ                                └────────┘     └─────────┘          
257  hf.of_eq $ λ ⟨a, b⟩, rfl
id   └┘└────┘            └─┘
src    └────┘             └─┘
typ  └┘└────┘            └─┘
258  
259  protected theorem id : computable (@id α) := primrec.id.to_comp
id                          └────────┘   └┘      └────────┘└──────┘
src                         └────────┘   └┘       └────────┘└──────┘
typ                         └────────┘   └┘      └────────┘└──────┘
260  
261  theorem fst : computable (@prod.fst α β) := primrec.fst.to_comp
id                 └────────┘   └──────┘       └─────────┘└──────┘
src                └────────┘   └──────┘         └─────────┘└──────┘
typ                └────────┘   └──────┘       └─────────┘└──────┘
262  
263  theorem snd : computable (@prod.snd α β) := primrec.snd.to_comp
id                 └────────┘   └──────┘       └─────────┘└──────┘
src                └────────┘   └──────┘         └─────────┘└──────┘
typ                └────────┘   └──────┘       └─────────┘└──────┘
264  
265  theorem pair {f : α → β} {g : α → γ}
id                                  
typ                                 
266    (hf : computable f) (hg : computable g) : computable (λ a, (f a, g a)) :=
id           └────────┘         └────────┘     └────────┘          
src          └────────┘          └────────┘      └────────┘       
typ          └────────┘         └────────┘     └────────┘          
267  (hf.pair hg).of_eq $
id    └┘└───┘ └┘ └───┘
src     └───┘    └───┘
typ   └┘└───┘ └┘ └───┘
268  λ n, by cases decode α n; simp [(<*>)]
id                └────┘  
src          └────┘└────┘    └────┘ └─────
typ         └────┘└────┘  └────┘ └─────
doc          └────┘          └────┘ └─────
txt          └────┘          └────┘ └─────
par          └────┘          └────┘ └─────
pid                              └───┘
st          └───────────────────────────────
269  
src  
typ  
doc  
txt  
par  
pid  
st   
270  theorem unpair : computable nat.unpair := primrec.unpair.to_comp
id                    └────────┘ └────────┘    └────────────┘└──────┘
src                   └────────┘ └────────┘    └────────────┘└──────┘
typ                   └────────┘ └────────┘    └────────────┘└──────┘
doc                              └────────┘
271  
272  theorem succ : computable nat.succ := primrec.succ.to_comp
id                  └────────┘ └──────┘    └──────────┘└──────┘
src                 └────────┘ └──────┘    └──────────┘└──────┘
typ                 └────────┘ └──────┘    └──────────┘└──────┘
273  theorem pred : computable nat.pred := primrec.pred.to_comp
id                  └────────┘ └──────┘    └──────────┘└──────┘
src                 └────────┘ └──────┘    └──────────┘└──────┘
typ                 └────────┘ └──────┘    └──────────┘└──────┘
274  theorem nat_bodd : computable nat.bodd := primrec.nat_bodd.to_comp
id                      └────────┘ └──────┘    └──────────────┘└──────┘
src                     └────────┘ └──────┘    └──────────────┘└──────┘
typ                     └────────┘ └──────┘    └──────────────┘└──────┘
275  theorem nat_div2 : computable nat.div2 := primrec.nat_div2.to_comp
id                      └────────┘ └──────┘    └──────────────┘└──────┘
src                     └────────┘ └──────┘    └──────────────┘└──────┘
typ                     └────────┘ └──────┘    └──────────────┘└──────┘
276  
277  theorem sum_inl : computable (@sum.inl α β) := primrec.sum_inl.to_comp
id                     └────────┘   └─────┘       └─────────────┘└──────┘
src                    └────────┘   └─────┘         └─────────────┘└──────┘
typ                    └────────┘   └─────┘       └─────────────┘└──────┘
278  theorem sum_inr : computable (@sum.inr α β) := primrec.sum_inr.to_comp
id                     └────────┘   └─────┘       └─────────────┘└──────┘
src                    └────────┘   └─────┘         └─────────────┘└──────┘
typ                    └────────┘   └─────┘       └─────────────┘└──────┘
279  
280  theorem list_cons : computable₂ (@list.cons α) := primrec.list_cons.to_comp
id                       └─────────┘   └───────┘      └───────────────┘└──────┘
src                      └─────────┘   └───────┘       └───────────────┘└──────┘
typ                      └─────────┘   └───────┘      └───────────────┘└──────┘
281  theorem list_reverse : computable (@list.reverse α) := primrec.list_reverse.to_comp
id                          └────────┘   └──────────┘      └──────────────────┘└──────┘
src                         └────────┘   └──────────┘       └──────────────────┘└──────┘
typ                         └────────┘   └──────────┘      └──────────────────┘└──────┘
282  theorem list_nth : computable₂ (@list.nth α) := primrec.list_nth.to_comp
id                      └─────────┘   └──────┘      └──────────────┘└──────┘
src                     └─────────┘   └──────┘       └──────────────┘└──────┘
typ                     └─────────┘   └──────┘      └──────────────┘└──────┘
283  theorem list_append : computable₂ ((++) : list α → list α → list α) := primrec.list_append.to_comp
id                         └─────────┘        └──┘    └──┘    └──┘      └─────────────────┘└──────┘
src                        └─────────┘        └──┘     └──┘     └──┘       └─────────────────┘└──────┘
typ                        └─────────┘        └──┘    └──┘    └──┘      └─────────────────┘└──────┘
284  theorem list_concat : computable₂ (λ l (a:α), l ++ [a]) := primrec.list_concat.to_comp
id                         └─────────┘            └┘      └─────────────────┘└──────┘
src                        └─────────┘               └┘       └─────────────────┘└──────┘
typ                        └─────────┘            └┘      └─────────────────┘└──────┘
285  theorem list_length : computable (@list.length α) := primrec.list_length.to_comp
id                         └────────┘   └─────────┘      └─────────────────┘└──────┘
src                        └────────┘   └─────────┘       └─────────────────┘└──────┘
typ                        └────────┘   └─────────┘      └─────────────────┘└──────┘
286  
287  theorem vector_cons {n} : computable₂ (@vector.cons α n) := primrec.vector_cons.to_comp
id                             └─────────┘   └─────────┘       └─────────────────┘└──────┘
src                            └─────────┘   └─────────┘         └─────────────────┘└──────┘
typ                            └─────────┘   └─────────┘       └─────────────────┘└──────┘
288  theorem vector_to_list {n} : computable (@vector.to_list α n) := primrec.vector_to_list.to_comp
id                                └────────┘   └────────────┘       └────────────────────┘└──────┘
src                               └────────┘   └────────────┘         └────────────────────┘└──────┘
typ                               └────────┘   └────────────┘       └────────────────────┘└──────┘
289  theorem vector_length {n} : computable (@vector.length α n) := primrec.vector_length.to_comp
id                               └────────┘   └───────────┘       └───────────────────┘└──────┘
src                              └────────┘   └───────────┘         └───────────────────┘└──────┘
typ                              └────────┘   └───────────┘       └───────────────────┘└──────┘
290  theorem vector_head {n} : computable (@vector.head α n) := primrec.vector_head.to_comp
id                             └────────┘   └─────────┘       └─────────────────┘└──────┘
src                            └────────┘   └─────────┘         └─────────────────┘└──────┘
typ                            └────────┘   └─────────┘       └─────────────────┘└──────┘
291  theorem vector_tail {n} : computable (@vector.tail α n) := primrec.vector_tail.to_comp
id                             └────────┘   └─────────┘       └─────────────────┘└──────┘
src                            └────────┘   └─────────┘         └─────────────────┘└──────┘
typ                            └────────┘   └─────────┘       └─────────────────┘└──────┘
292  theorem vector_nth {n} : computable₂ (@vector.nth α n) := primrec.vector_nth.to_comp
id                            └─────────┘   └────────┘       └────────────────┘└──────┘
src                           └─────────┘   └────────┘         └────────────────┘└──────┘
typ                           └─────────┘   └────────┘       └────────────────┘└──────┘
293  theorem vector_nth' {n} : computable (@vector.nth α n) := primrec.vector_nth'.to_comp
id                             └────────┘   └────────┘       └─────────────────┘└──────┘
src                            └────────┘   └────────┘         └─────────────────┘└──────┘
typ                            └────────┘   └────────┘       └─────────────────┘└──────┘
294  theorem vector_of_fn' {n} : computable (@vector.of_fn α n) := primrec.vector_of_fn'.to_comp
id                               └────────┘   └──────────┘       └───────────────────┘└──────┘
src                              └────────┘   └──────────┘         └───────────────────┘└──────┘
typ                              └────────┘   └──────────┘       └───────────────────┘└──────┘
295  
296  theorem fin_app {n} : computable₂ (@id (fin n → σ)) := primrec.fin_app.to_comp
id                         └─────────┘   └┘  └─┘          └─────────────┘└──────┘
src                        └─────────┘   └┘  └─┘            └─────────────┘└──────┘
typ                        └─────────┘   └┘  └─┘          └─────────────┘└──────┘
297  
298  protected theorem encode : computable (@encode α _) :=
id                              └────────┘   └────┘ 
src                             └────────┘   └────┘
typ                             └────────┘   └────┘ 
299  primrec.encode.to_comp
id   └────────────┘└──────┘
src  └────────────┘└──────┘
typ  └────────────┘└──────┘
300  
301  protected theorem decode : computable (decode α) :=
id                              └────────┘  └────┘ 
src                             └────────┘  └────┘
typ                             └────────┘  └────┘ 
302  primrec.decode.to_comp
id   └────────────┘└──────┘
src  └────────────┘└──────┘
typ  └────────────┘└──────┘
303  
304  protected theorem of_nat (α) [denumerable α] : computable (of_nat α) :=
id                                 └─────────┘     └────────┘  └────┘ 
src                                └─────────┘      └────────┘  └────┘
typ                                └─────────┘     └────────┘  └────┘ 
doc                                └─────────┘
305  (primrec.of_nat _).to_comp
id    └────────────┘   └─────┘
src   └────────────┘   └─────┘
typ   └────────────┘   └─────┘
306  
307  theorem encode_iff {f : α → σ} : computable (λ a, encode (f a)) ↔ computable f :=
id                                  └────────┘      └────┘       └────────┘ 
src                                   └────────┘       └────┘         └────────┘
typ                                 └────────┘      └────┘       └────────┘ 
308  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
309  
310  theorem option_some : computable (@option.some α) :=
id                         └────────┘   └─────────┘ 
src                        └────────┘   └─────────┘
typ                        └────────┘   └─────────┘ 
311  primrec.option_some.to_comp
id   └─────────────────┘└──────┘
src  └─────────────────┘└──────┘
typ  └─────────────────┘└──────┘
312  
313  end computable
314  
315  namespace partrec
316  variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
317  variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id              └─────────┘     └─────────┘     └─────────┘     └─────────┘
src             └─────────┘     └─────────┘     └─────────┘     └─────────┘
typ             └─────────┘     └─────────┘     └─────────┘     └─────────┘
doc             └─────────┘     └─────────┘     └─────────┘     └─────────┘
318  
319  open computable
320  
321  theorem of_eq {f g : α →. σ} (hf : partrec f) (H : ∀ n, f n = g n) : partrec g :=
id                         └┘         └─────┘                    └─────┘ 
src                         └┘          └─────┘                          └─────┘
typ                        └┘         └─────┘                    └─────┘ 
doc                         └┘
322  (funext H : f = g) ▸ hf
id    └────┘         └┘
src   └────┘           
typ   └────┘         └┘
323  
324  theorem of_eq_tot {f : α →. σ} {g : α → σ}
id                           └┘           
src                           └┘
typ                          └┘           
doc                           └┘
325    (hf : partrec f) (H : ∀ n, g n ∈ f n) : computable g :=
id           └─────┘                    └────────┘ 
src          └─────┘                          └────────┘
typ          └─────┘                    └────────┘ 
326  hf.of_eq (λ a, eq_some_iff.2 (H a))
id   └┘└────┘      └─────────┘    
src    └────┘       └─────────┘
typ  └┘└────┘      └─────────┘    
327  
328  theorem none : partrec (λ a : α, @roption.none σ) :=
id                  └─────┘           └──────────┘ 
src                 └─────┘            └──────────┘
typ                 └─────┘           └──────────┘ 
doc                                    └──────────┘
329  nat.partrec.none.of_eq $ λ n, by cases decode α n; simp
id   └──────────────┘└────┘                └────┘  
src  └──────────────┘└────┘           └────┘└────┘    └────
typ  └──────────────┘└────┘          └────┘└────┘  └────
doc                                   └────┘          └────
txt                                   └────┘          └────
par                                   └────┘          └────
pid                                                      
st                                   └───────────────────────
330  
src  
typ  
doc  
txt  
par  
pid  
st   
331  protected theorem some : partrec (@roption.some α) := computable.id
id                            └─────┘   └──────────┘      └───────────┘
src                           └─────┘   └──────────┘       └───────────┘
typ                           └─────┘   └──────────┘      └───────────┘
doc                                     └──────────┘
332  
333  theorem const' (s : roption σ) : partrec (λ a : α, s) :=
id                       └─────┘     └─────┘          
src                      └─────┘      └─────┘
typ                      └─────┘     └─────┘          
doc                      └─────┘
334  by haveI := classical.dec s.dom; exact
id               └───────────┘ └───┘
src     └───────┘└───────────┘└───┘  └────┘
typ     └───────┘└───────────┘└───┘  └────┘
doc     └───────┘                    └────┘
txt     └───────┘                    └────┘
par     └───────┘                    └────┘
pid          └─┘                         
st     └────────────────────────────────────
335  (of_option (const (to_option s))).of_eq (λ a, of_to_option s)
id    └───────┘  └───┘  └───────┘                  └──────────┘ 
src   └───────┘ └───┘ └───────┘ └────────┘  └──┘└──────────┘ └─
typ   └───────┘ └───┘ └───────┘ └────────┘  └──┘└──────────┘└─
doc                   └───────┘ └────────┘  └──┘             └─
txt                             └────────┘  └──┘             └─
par                             └────────┘  └──┘             └─
pid                             └────────┘  └──┘             
st   ──────────────────────────────────────────────────────────────
336  
src  
typ  
doc  
txt  
par  
pid  
st   
337  protected theorem bind {f : α →. β} {g : α → β →. σ}
id                                └┘            └┘ 
src                                └┘               └┘
typ                               └┘            └┘ 
doc                                └┘               └┘
338    (hf : partrec f) (hg : partrec₂ g) : partrec (λ a, (f a).bind (g a)) :=
id           └─────┘         └──────┘     └─────┘         └──┘    
src          └─────┘          └──────┘      └─────┘            └──┘
typ          └─────┘         └──────┘     └─────┘         └──┘    
doc                                                            └──┘
339  (hg.comp (nat.partrec.some.pair hf)).of_eq $
id    └┘└───┘  └──────────────┘└───┘ └┘  └───┘
src     └───┘  └──────────────┘└───┘     └───┘
typ   └┘└───┘  └──────────────┘└───┘ └┘  └───┘
340  λ n, by simp [(<*>)]; cases e : decode α n with a;
id                                  └────┘  
src          └────┘ └───┘  └────┘ └─┘└────┘  └─────┘
typ         └────┘ └───┘  └────┘ └─┘└────┘└─────┘
doc          └────┘ └───┘  └────┘ └─┘        └─────┘
txt          └────┘ └───┘  └────┘ └─┘        └─────┘
par          └────┘ └───┘  └────┘ └─┘        └─────┘
pid               └───┘        └─┘        └─────┘
st          └───────────────────────────────────────────
341    simp [e, encodek]
id             └─────┘
src    └────┘ └┘└─────┘└─
typ    └────┘└┘└─────┘└─
doc    └────┘ └┘       └─
txt    └────┘ └┘       └─
par    └────┘ └┘       └─
pid         └┘       
st   ────────────────────
342  
src  
typ  
doc  
txt  
par  
pid  
st   
343  theorem map {f : α →. β} {g : α → β → σ}
id                     └┘              
src                     └┘
typ                    └┘              
doc                     └┘
344    (hf : partrec f) (hg : computable₂ g) : partrec (λ a, (f a).map (g a)) :=
id           └─────┘         └─────────┘     └─────┘         └─┘    
src          └─────┘          └─────────┘      └─────┘            └─┘
typ          └─────┘         └─────────┘     └─────┘         └─┘    
doc                                                               └─┘
345  by simpa [bind_some_eq_map] using
id             └──────────────┘
src     └─────┘└──────────────┘└───────
typ     └─────┘└──────────────┘└───────
doc     └─────┘                └───────
txt     └─────┘                └───────
par     └─────┘                └───────
pid                          └─────
st     └───────────────────────────────
346     @@partrec.bind _ _ _ (λ a b, roption.some (g a b)) hf hg
id        └──────────┘               └──────────┘         └┘ └┘
src  ──┘  └──────────┘└─────┘  └────┘└──────────┘    └─┘    
typ  ──┘  └──────────┘└─────┘  └────┘└──────────┘   └─┘└┘└┘
doc  ──┘              └─────┘  └────┘└──────────┘    └─┘    
txt  ──┘              └─────┘  └────┘                └─┘    
par  ──┘              └─────┘  └────┘                └─┘    
pid  ──┘              └─────┘  └────┘                └─┘    
st   ────────────────────────────────────────────────────────────
347  
src  
typ  
doc  
txt  
par  
pid  
st   
348  theorem to₂ {f : α × β →. σ} (hf : partrec f) : partrec₂ (λ a b, f (a, b)) :=
id                       └┘         └─────┘     └──────┘          
src                        └┘          └─────┘      └──────┘           
typ                      └┘         └─────┘     └──────┘          
doc                         └┘
349  hf.of_eq $ λ ⟨a, b⟩, rfl
id   └┘└────┘            └─┘
src    └────┘             └─┘
typ  └┘└────┘            └─┘
350  
351  theorem nat_elim
352    {f : α → ℕ} {g : α →. σ} {h : α → ℕ × σ →. σ}
id                     └┘              └┘ 
src                      └┘                 └┘
typ                    └┘              └┘ 
doc                       └┘                   └┘
353    (hf : computable f) (hg : partrec g) (hh : partrec₂ h) :
id           └────────┘         └─────┘         └──────┘ 
src          └────────┘          └─────┘          └──────┘
typ          └────────┘         └─────┘         └──────┘ 
354    partrec (λ a, (f a).elim (g a) (λ y IH, IH.bind (λ i, h a (y, i)))) :=
id     └─────┘         └──┘          └┘  └┘└───┘          
src    └─────┘            └──┘                   └───┘           
typ    └─────┘         └──┘          └┘  └┘└───┘          
doc                                              └───┘
355  (nat.partrec.prec' hf hg hh).of_eq $ λ n, begin
id    └───────────────┘ └┘ └┘ └┘ └───┘      
src   └───────────────┘          └───┘
typ   └───────────────┘ └┘ └┘ └┘ └───┘      
st                                             └─────
356    cases e : decode α n with a; simp [e],
id               └────┘                 
src    └────┘ └─┘└────┘  └─────┘  └────┘ 
typ    └────┘ └─┘└────┘└─────┘  └────┘
doc    └────┘ └─┘        └─────┘  └────┘ 
txt    └────┘ └─┘        └─────┘  └────┘ 
par    └────┘ └─┘        └─────┘  └────┘ 
pid          └─┘        └─────┘       
st   ──────────────────────────────────────┘└─
357    induction f a with m IH; simp,
id                
src    └────────┘  └────────┘  └──┘
typ    └────────┘└────────┘  └──┘
doc    └────────┘  └────────┘  └──┘
txt    └────────┘  └────────┘  └──┘
par    └────────┘  └────────┘  └──┘
pid               └───────┘
st   ──────────────────────────────┘└─
358    rw [IH, bind_map],
id         └┘  └──────┘
src    └──┘  └┘└──────┘
typ    └──┘└┘└┘└──────┘
doc    └──┘  └┘        
txt    └──┘  └┘        
par    └──┘  └┘        
pid      └┘  └┘        
st   ───────┘└────────┘└─
359    congr, funext s,
src    └───┘  └──────┘
typ    └───┘  └──────┘
doc           └──────┘
txt    └───┘  └──────┘
par    └───┘  └──────┘
pid                 └┘
st   ──────┘└────────┘└─
360    simp [encodek]
id           └─────┘
src    └────┘└─────┘└┘
typ    └────┘└─────┘└┘
doc    └────┘       └┘
txt    └────┘       └┘
par    └────┘       └┘
pid               
st   ────────────────┘
361  end
st   └─┘
362  
363  theorem comp {f : β →. σ} {g : α → β}
id                      └┘           
src                      └┘
typ                     └┘           
doc                      └┘
364    (hf : partrec f) (hg : computable g) : partrec (λ a, f (g a)) :=
id           └─────┘         └────────┘     └─────┘         
src          └─────┘          └────────┘      └─────┘
typ          └─────┘         └────────┘     └─────┘         
365  (hf.comp hg).of_eq $
id    └┘└───┘ └┘ └───┘
src     └───┘    └───┘
typ   └┘└───┘ └┘ └───┘
366  λ n, by simp; cases e : decode α n with a;
id                          └────┘  
src          └──┘  └────┘ └─┘└────┘  └─────┘
typ         └──┘  └────┘ └─┘└────┘└─────┘
doc          └──┘  └────┘ └─┘        └─────┘
txt          └──┘  └────┘ └─┘        └─────┘
par          └──┘  └────┘ └─┘        └─────┘
pid                      └─┘        └─────┘
st          └───────────────────────────────────
367    simp [e, encodek]
id             └─────┘
src    └────┘ └┘└─────┘└─
typ    └────┘└┘└─────┘└─
doc    └────┘ └┘       └─
txt    └────┘ └┘       └─
par    └────┘ └┘       └─
pid         └┘       
st   ────────────────────
368  
src  
typ  
doc  
txt  
par  
pid  
st   
369  theorem nat_iff {f : ℕ →. ℕ} : partrec f ↔ nat.partrec f :=
id                         └┘     └─────┘   └─────────┘ 
src                        └┘     └─────┘    └─────────┘
typ                        └┘     └─────┘   └─────────┘ 
doc                         └┘
370  by simp [partrec, map_id']
id            └─────┘  └─────┘
src     └────┘└─────┘└┘└─────┘└─
typ     └────┘└─────┘└┘└─────┘└─
doc     └────┘       └┘       └─
txt     └────┘       └┘       └─
par     └────┘       └┘       └─
pid                └┘       
st     └────────────────────────
371  
src  
typ  
doc  
txt  
par  
pid  
st   
372  theorem map_encode_iff {f : α →. σ} : partrec (λ a, (f a).map encode) ↔ partrec f :=
id                                └┘     └─────┘         └─┘  └────┘   └─────┘ 
src                                └┘      └─────┘            └─┘  └────┘   └─────┘
typ                               └┘     └─────┘         └─┘  └────┘   └─────┘ 
doc                                └┘                         └─┘
373  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
374  
375  end partrec
376  
377  namespace partrec₂
378  variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {σ : Type*}
379  variables [primcodable α] [primcodable β] [primcodable γ] [primcodable δ] [primcodable σ]
id              └─────────┘     └─────────┘     └─────────┘     └─────────┘     └─────────┘
src             └─────────┘     └─────────┘     └─────────┘     └─────────┘     └─────────┘
typ             └─────────┘     └─────────┘     └─────────┘     └─────────┘     └─────────┘
doc             └─────────┘     └─────────┘     └─────────┘     └─────────┘     └─────────┘
380  
381  theorem unpaired {f : ℕ → ℕ →. α} : partrec (nat.unpaired f) ↔ partrec₂ f :=
id                             └┘     └─────┘  └──────────┘    └──────┘ 
src                            └┘      └─────┘  └──────────┘     └──────┘
typ                            └┘     └─────┘  └──────────┘    └──────┘ 
doc                              └┘
382  ⟨λ h, by simpa using h.comp primrec₂.mkpair.to_comp,
id                       └────┘ └─────────────────────┘
src           └──────────┘└────┘└─────────────────────┘
typ          └──────────┘└────┘└─────────────────────┘
doc           └──────────┘      
txt           └──────────┘      
par           └──────────┘      
pid                └────┘      
st           └─────────────────────────────────────────┘
383   λ h, h.comp primrec.unpair.to_comp⟩
id        └───┘ └────────────┘└──────┘
src         └───┘ └────────────┘└──────┘
typ       └───┘ └────────────┘└──────┘
384  
385  theorem unpaired' {f : ℕ → ℕ →. ℕ} : nat.partrec (nat.unpaired f) ↔ partrec₂ f :=
id                              └┘     └─────────┘  └──────────┘    └──────┘ 
src                             └┘     └─────────┘  └──────────┘     └──────┘
typ                             └┘     └─────────┘  └──────────┘    └──────┘ 
doc                               └┘
386  partrec.nat_iff.symm.trans unpaired
id   └─────────────┘└───┘└────┘ └──────┘
src  └─────────────┘└───┘└────┘ └──────┘
typ  └─────────────┘└───┘└────┘ └──────┘
387  
388  theorem comp
389    {f : β → γ →. σ} {g : α → β} {h : α → γ}
id              └┘                     
src               └┘
typ             └┘                     
doc               └┘
390    (hf : partrec₂ f) (hg : computable g) (hh : computable h) :
id           └──────┘         └────────┘         └────────┘ 
src          └──────┘          └────────┘          └────────┘
typ          └──────┘         └────────┘         └────────┘ 
391    partrec (λ a, f (g a) (h a)) := hf.comp (hg.pair hh)
id     └─────┘                   └┘└───┘  └┘└───┘ └┘
src    └─────┘                           └───┘    └───┘
typ    └─────┘                   └┘└───┘  └┘└───┘ └┘
392  
393  theorem comp₂
394    {f : γ → δ →. σ} {g : α → β → γ} {h : α → β → δ}
id              └┘                           
src               └┘
typ             └┘                           
doc               └┘
395    (hf : partrec₂ f) (hg : computable₂ g) (hh : computable₂ h) :
id           └──────┘         └─────────┘         └─────────┘ 
src          └──────┘          └─────────┘          └─────────┘
typ          └──────┘         └─────────┘         └─────────┘ 
396    partrec₂ (λ a b, f (g a b) (h a b)) := hf.comp hg hh
id     └──────┘                      └┘└───┘ └┘ └┘
src    └──────┘                                 └───┘
typ    └──────┘                      └┘└───┘ └┘ └┘
397  
398  end partrec₂
399  
400  namespace computable
401  variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
402  variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id              └─────────┘     └─────────┘     └─────────┘     └─────────┘
src             └─────────┘     └─────────┘     └─────────┘     └─────────┘
typ             └─────────┘     └─────────┘     └─────────┘     └─────────┘
doc             └─────────┘     └─────────┘     └─────────┘     └─────────┘
403  
404  theorem comp {f : β → σ} {g : α → β}
id                                  
typ                                 
405    (hf : computable f) (hg : computable g) :
id           └────────┘         └────────┘ 
src          └────────┘          └────────┘
typ          └────────┘         └────────┘ 
406    computable (λ a, f (g a)) := hf.comp hg
id     └────────┘               └┘└───┘ └┘
src    └────────┘                     └───┘
typ    └────────┘               └┘└───┘ └┘
407  
408  theorem comp₂ {f : γ → σ} {g : α → β → γ}
id                                      
typ                                     
409    (hf : computable f) (hg : computable₂ g) :
id           └────────┘         └─────────┘ 
src          └────────┘          └─────────┘
typ          └────────┘         └─────────┘ 
410    computable₂ (λ a b, f (g a b)) := hf.comp hg
id     └─────────┘                 └┘└───┘ └┘
src    └─────────┘                         └───┘
typ    └─────────┘                 └┘└───┘ └┘
411  
412  end computable
413  
414  namespace computable₂
415  variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {σ : Type*}
416  variables [primcodable α] [primcodable β] [primcodable γ] [primcodable δ] [primcodable σ]
id              └─────────┘     └─────────┘     └─────────┘     └─────────┘     └─────────┘
src             └─────────┘     └─────────┘     └─────────┘     └─────────┘     └─────────┘
typ             └─────────┘     └─────────┘     └─────────┘     └─────────┘     └─────────┘
doc             └─────────┘     └─────────┘     └─────────┘     └─────────┘     └─────────┘
417  
418  theorem comp
419    {f : β → γ → σ} {g : α → β} {h : α → γ}
id                                    
typ                                   
420    (hf : computable₂ f) (hg : computable g) (hh : computable h) :
id           └─────────┘         └────────┘         └────────┘ 
src          └─────────┘          └────────┘          └────────┘
typ          └─────────┘         └────────┘         └────────┘ 
421    computable (λ a, f (g a) (h a)) := hf.comp (hg.pair hh)
id     └────────┘                   └┘└───┘  └┘└───┘ └┘
src    └────────┘                           └───┘    └───┘
typ    └────────┘                   └┘└───┘  └┘└───┘ └┘
422  
423  theorem comp₂
424    {f : γ → δ → σ} {g : α → β → γ} {h : α → β → δ}
id                                          
typ                                         
425    (hf : computable₂ f) (hg : computable₂ g) (hh : computable₂ h) :
id           └─────────┘         └─────────┘         └─────────┘ 
src          └─────────┘          └─────────┘          └─────────┘
typ          └─────────┘         └─────────┘         └─────────┘ 
426    computable₂ (λ a b, f (g a b) (h a b)) := hf.comp hg hh
id     └─────────┘                      └┘└───┘ └┘ └┘
src    └─────────┘                                 └───┘
typ    └─────────┘                      └┘└───┘ └┘ └┘
427  
428  end computable₂
429  
430  namespace partrec
431  variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
id             
typ            
432  variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id              └─────────┘     └─────────┘     └─────────┘     └─────────┘
src             └─────────┘     └─────────┘     └─────────┘     └─────────┘
typ             └─────────┘     └─────────┘     └─────────┘     └─────────┘
doc             └─────────┘     └─────────┘     └─────────┘     └─────────┘
433  
434  open computable
435  
436  theorem rfind {p : α → ℕ →. bool} (hp : partrec₂ p) :
id                          └┘ └──┘        └──────┘ 
src                          └┘ └──┘        └──────┘
typ                         └┘ └──┘        └──────┘ 
doc                           └┘
437    partrec (λ a, nat.rfind (p a)) :=
id     └─────┘      └───────┘   
src    └─────┘       └───────┘
typ    └─────┘      └───────┘   
438  (nat.partrec.rfind $ hp.map
id    └───────────────┘   └┘└──┘
src   └───────────────┘     └──┘
typ   └───────────────┘   └┘└──┘
439    ((primrec.dom_bool (λ b, cond b 0 1))
id       └──────────────┘      └──┘ 
src      └──────────────┘       └──┘
typ      └──────────────┘      └──┘ 
440      .comp primrec.snd).to₂.to_comp).of_eq $
id       └──┘  └─────────┘ └─┘ └─────┘  └───┘
src      └──┘  └─────────┘ └─┘ └─────┘  └───┘
typ      └──┘  └─────────┘ └─┘ └─────┘  └───┘
441  λ n, begin
id     
typ    
st        └─────
442    cases e : decode α n with a;
id               └────┘  
src    └────┘ └─┘└────┘  └─────┘
typ    └────┘ └─┘└────┘└─────┘
doc    └────┘ └─┘        └─────┘
txt    └────┘ └─┘        └─────┘
par    └────┘ └─┘        └─────┘
pid          └─┘        └─────┘
st   ───────────────────────────────
443      simp [e, nat.rfind_zero_none, map_id'],
id               └─────────────────┘  └─────┘
src      └────┘ └┘└─────────────────┘└┘└─────┘
typ      └────┘└┘└─────────────────┘└┘└─────┘
doc      └────┘ └┘                   └┘       
txt      └────┘ └┘                   └┘       
par      └────┘ └┘                   └┘       
pid           └┘                   └┘       
st   ─────────────────────────────────────────┘└─
444    congr, funext n,
src    └───┘  └──────┘
typ    └───┘  └──────┘
doc           └──────┘
txt    └───┘  └──────┘
par    └───┘  └──────┘
pid                 └┘
st   ──────┘└────────┘└─
445    simp [roption.map_map, (∘)],
id           └─────────────┘  
src    └────┘└─────────────┘└┘└─┘
typ    └────┘└─────────────┘└┘└─┘
doc    └────┘               └┘ └─┘
txt    └────┘               └┘ └─┘
par    └────┘               └┘ └─┘
pid                       └┘ └─┘
st   ────────────────────────────┘└─
446    apply map_id' (λ b, _),
id           └─────┘
src    └────┘└─────┘  └────┘
typ    └────┘└─────┘  └────┘
doc    └────┘         └────┘
txt    └────┘         └────┘
par    └────┘         └────┘
pid                  └────┘
st   ───────────────────────┘└─
447    cases b; refl
id           
src    └────┘   └───┘
typ    └────┘  └───┘
doc    └────┘   └───┘
txt    └────┘   └───┘
par    └────┘   └───┘
pid                
st   ───────────────┘
448  end
st   └─┘
449  
450  theorem rfind_opt {f : α → ℕ → option σ} (hf : computable₂ f) :
id                                └────┘         └─────────┘ 
src                                └────┘          └─────────┘
typ                               └────┘         └─────────┘ 
451    partrec (λ a, nat.rfind_opt (f a)) :=
id     └─────┘      └───────────┘   
src    └─────┘       └───────────┘
typ    └─────┘      └───────────┘   
452  (rfind (primrec.option_is_some.to_comp.comp hf).part.to₂).bind
id    └───┘  └────────────────────┘└──────┘└───┘ └┘ └──┘ └─┘  └──┘
src   └───┘  └────────────────────┘└──────┘└───┘    └──┘ └─┘  └──┘
typ   └───┘  └────────────────────┘└──────┘└───┘ └┘ └──┘ └─┘  └──┘
453    (of_option hf)
id      └───────┘ └┘
src     └───────┘
typ     └───────┘ └┘
454  
455  theorem nat_cases_right
456    {f : α → ℕ} {g : α → σ} {h : α → ℕ →. σ}
id                                  └┘ 
src                                     └┘
typ                                 └┘ 
doc                                       └┘
457    (hf : computable f) (hg : computable g) (hh : partrec₂ h) :
id           └────────┘         └────────┘         └──────┘ 
src          └────────┘          └────────┘          └──────┘
typ          └────────┘         └────────┘         └──────┘ 
458    partrec (λ a, (f a).cases (some (g a)) (h a)) :=
id     └─────┘         └───┘   └──┘        
src    └─────┘            └───┘   └──┘
typ    └─────┘         └───┘   └──┘        
doc                               └──┘
459  (nat_elim hf hg (hh.comp fst (pred.comp $ hf.comp fst)).to₂).of_eq $
id    └──────┘ └┘ └┘  └┘└───┘ └─┘  └──┘└───┘   └┘└───┘ └─┘  └─┘  └───┘
src   └──────┘          └───┘ └─┘  └──┘└───┘     └───┘ └─┘  └─┘  └───┘
typ   └──────┘ └┘ └┘  └┘└───┘ └─┘  └──┘└───┘   └┘└───┘ └─┘  └─┘  └───┘
460  λ a, begin
id     
typ    
st        └─────
461    simp, cases f a; simp,
id                  
src    └──┘  └────┘    └──┘
typ    └──┘  └────┘  └──┘
doc    └──┘  └────┘    └──┘
txt    └──┘  └────┘    └──┘
par    └──┘  └────┘    └──┘
pid                
st   ─────┘└───────────────┘└─
462    refine ext (λ b, ⟨λ H, _, λ H, _⟩),
id            └─┘
src    └─────┘└─┘  └──┘  └─────┘ └─────┘
typ    └─────┘└─┘  └──┘  └─────┘ └─────┘
doc    └─────┘└─┘  └──┘  └─────┘ └─────┘
txt    └─────┘     └──┘  └─────┘ └─────┘
par    └─────┘     └──┘  └─────┘ └─────┘
pid               └──┘  └─────┘ └─────┘
st   ───────────────────────────────────┘└─
463    { rcases mem_bind_iff.1 H with ⟨c, h₁, h₂⟩, exact h₂ },
id              └──────────┘                            └┘
src      └─────┘└──────────┘└─┘ └───────────────┘  └────┘  
typ      └─────┘└──────────┘└─┘└───────────────┘  └────┘└┘
doc      └─────┘            └─┘ └───────────────┘  └────┘  
txt      └─────┘            └─┘ └───────────────┘  └────┘  
par      └─────┘            └─┘ └───────────────┘  └────┘  
pid                        └─┘ └───────────────┘         
st   ───┘└──────────────────────────────────────┘└─────────┘└┘
464    { have : ∀ m, (nat.elim (roption.some (g a))
id                    └──────┘  └──────────┘  
src      └─────┘ └┘  └──────┘ └──────────┘   └──
typ      └─────┘ └┘  └──────┘ └──────────┘  └──
doc      └─────┘ └┘           └──────────┘   └──
txt      └─────┘ └┘                          └──
par      └─────┘ └┘                          └──
pid      └───┘└┘ └┘                          └──
st   ───────────────────────────────────────────────
465        (λ y IH, IH.bind (λ _, h a n)) m).dom,
id                    └───┘         
src  ─────┘  └─────┘  └───┘  └──┘   └─┘ └───┘
typ  ─────┘  └─────┘  └───┘  └──┘└─┘ └───┘
doc  ─────┘  └─────┘  └───┘  └──┘   └─┘ └───┘
txt  ─────┘  └─────┘         └──┘   └─┘ └───┘
par  ─────┘  └─────┘         └──┘   └─┘ └───┘
pid  ─────┘  └─────┘         └──┘   └─┘ └──┘
st   ──────────────────────────────────────────┘└─
466      { intro, induction m; simp [*, H.fst] },
id                          
src        └───┘  └────────┘   └───────┘     └┘
typ        └───┘  └────────┘  └───────┘└───┘└┘
doc        └───┘  └────────┘   └───────┘     └┘
txt        └───┘  └────────┘   └───────┘     └┘
par        └───┘  └────────┘   └───────┘     └┘
pid                               └──┘     
st   ─────┘└───┘└─────────────────────────────┘└┘
467      exact ⟨⟨this n, H.fst⟩, H.snd⟩ }
id               └──┘   └───┘   └───┘
src      └────┘       └┘└───┘└─┘└───┘└┘
typ      └────┘  └──┘└┘└───┘└─┘└───┘└┘
doc      └────┘       └┘     └─┘     └┘
txt      └────┘       └┘     └─┘     └┘
par      └────┘       └┘     └─┘     └┘
pid                  └┘     └─┘     
st   ──────────────────────────────────┘└─
468  end
st   ──┘
469  
470  theorem bind_decode2_iff {f : α →. σ} : partrec f ↔
id                                  └┘     └─────┘  
src                                  └┘      └─────┘   
typ                                 └┘     └─────┘  
doc                                  └┘
471    nat.partrec (λ n, roption.bind (decode2 α n) (λ a, (f a).map encode)) :=
id     └─────────┘      └──────────┘  └─────┘            └─┘  └────┘
src    └─────────┘       └──────────┘  └─────┘                 └─┘  └────┘
typ    └─────────┘      └──────────┘  └─────┘            └─┘  └────┘
doc                      └──────────┘                          └─┘
472  ⟨λ hf, nat_iff.1 $ (of_option primrec.decode2.to_comp).bind $
id      └┘  └─────┘     └───────┘ └─────────────┘└──────┘ └──┘
src         └─────┘     └───────┘ └─────────────┘└──────┘ └──┘
typ     └┘  └─────┘     └───────┘ └─────────────┘└──────┘ └──┘
473    (map hf (computable.encode.comp snd).to₂).comp snd,
id      └─┘ └┘  └───────────────┘└───┘ └─┘ └─┘  └──┘  └─┘
src     └─┘     └───────────────┘└───┘ └─┘ └─┘  └──┘  └─┘
typ     └─┘ └┘  └───────────────┘└───┘ └─┘ └─┘  └──┘  └─┘
474  λ h, map_encode_iff.1 $ by simpa [encodek2]
id       └────────────┘              └──────┘
src       └────────────┘       └─────┘└──────┘└─
typ      └────────────┘       └─────┘└──────┘└─
doc                             └─────┘        └─
txt                             └─────┘        └─
par                             └─────┘        └─
pid                                          
st                             └─────────────────
475    using (nat_iff.2 h).comp (@computable.encode α _)⟩
id            └─────┘            └───────────────┘ 
src  ───────┘ └─────┘└─┘ └─────┘  └───────────────┘ └─┘
typ  ───────┘ └─────┘└─┘└─────┘  └───────────────┘└─┘
doc  ───────┘        └─┘ └─────┘                    └─┘
txt  ───────┘        └─┘ └─────┘                    └─┘
par  ───────┘        └─┘ └─────┘                    └─┘
pid  ─┘└────┘        └─┘ └─────┘                    └─┘
st   ──────────────────────────────────────────────────┘
476  
477  theorem vector_m_of_fn : ∀ {n} {f : fin n → α →. σ}, (∀ i, partrec (f i)) →
id                                     └─┘    └┘         └─────┘   
src                                      └─┘       └┘           └─────┘
typ                                    └─┘    └┘         └─────┘   
doc                                                └┘
478    partrec (λ (a : α), vector.m_of_fn (λ i, f i a))
id     └─────┘            └────────────┘        
src    └─────┘             └────────────┘
typ    └─────┘            └────────────┘        
479  | 0     f hf := const _
id                   └───┘
src                  └───┘
typ                  └───┘
480  | (n+1) f hf := by simp [vector.m_of_fn]; exact
id                           └────────────┘
src                    └────┘└────────────┘  └─────
typ                    └────┘└────────────┘  └─────
doc                     └────┘                └─────
txt                     └────┘                └─────
par                     └────┘                └─────
pid                                              
st                     └─────────────────────────────
481    (hf 0).bind (partrec.bind ((vector_m_of_fn (λ i, hf i.succ)).comp fst)
id                  └──────────┘   └────────────┘       └┘  └───┘
src  ─┘   └───────┘ └──────────┘                  └──┘   └───┘└──────┘   └─
typ  ─┘   └───────┘ └──────────┘  └────────────┘  └──┘└┘ └───┘└──────┘   └─
doc  ─┘   └───────┘                               └──┘        └──────┘   └─
txt  ─┘   └───────┘                               └──┘        └──────┘   └─
par  ─┘   └───────┘                               └──┘        └──────┘   └─
pid  ─┘   └───────┘                               └──┘        └──────┘   └─
st   ─────────────────────────────────────────────────────────────────────────
482      (primrec.vector_cons.to_comp.comp (snd.comp fst) snd))
id        └──────────────────────────────┘  └──────┘ └─┘  └─┘
src  ───┘ └──────────────────────────────┘ └──────┘└─┘└┘└─┘└──
typ  ───┘ └──────────────────────────────┘ └──────┘└─┘└┘└─┘└──
doc  ───┘                                             └┘   └──
txt  ───┘                                             └┘   └──
par  ───┘                                             └┘   └──
pid  ───┘                                             └┘   └┘
st   ───────────────────────────────────────────────────────────
483  
src  
typ  
doc  
txt  
par  
pid  
st   
484  end partrec
485  
486  @[simp] theorem vector.m_of_fn_roption_some {α n} : ∀ (f : fin n → α),
id                                                              └─┘   
src                                                             └─┘
typ                                                             └─┘   
doc    └──┘
487    vector.m_of_fn (λ i, roption.some (f i)) = roption.some (vector.of_fn f) :=
id     └────────────┘      └──────────┘       └──────────┘  └──────────┘ 
src    └────────────┘       └──────────┘         └──────────┘  └──────────┘
typ    └────────────┘      └──────────┘       └──────────┘  └──────────┘ 
doc                         └──────────┘          └──────────┘
488  vector.m_of_fn_pure
id   └─────────────────┘
src  └─────────────────┘
typ  └─────────────────┘
489  
490  namespace computable
491  variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
492  variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id              └─────────┘     └─────────┘     └─────────┘     └─────────┘
src             └─────────┘     └─────────┘     └─────────┘     └─────────┘
typ             └─────────┘     └─────────┘     └─────────┘     └─────────┘
doc             └─────────┘     └─────────┘     └─────────┘     └─────────┘
493  
494  theorem option_some_iff {f : α → σ} : computable (λ a, some (f a)) ↔ computable f :=
id                                       └────────┘      └──┘       └────────┘ 
src                                        └────────┘       └──┘         └────────┘
typ                                      └────────┘      └──┘       └────────┘ 
495  ⟨λ h, encode_iff.1 $ primrec.pred.to_comp.comp $ encode_iff.2 h,
id        └────────┘    └──────────┘└──────┘└───┘   └────────┘  
src        └────────┘    └──────────┘└──────┘└───┘   └────────┘
typ       └────────┘    └──────────┘└──────┘└───┘   └────────┘  
496   option_some.comp⟩
id    └─────────┘└───┘
src   └─────────┘└───┘
typ   └─────────┘└───┘
497  
498  theorem bind_decode_iff {f : α → β → option σ} : computable₂ (λ a n,
id                                      └────┘     └─────────┘     
src                                       └────┘      └─────────┘
typ                                     └────┘     └─────────┘     
499    (decode β n).bind (f a)) ↔ computable₂ f :=
id      └────┘   └──┘        └─────────┘ 
src     └────┘     └──┘          └─────────┘
typ     └────┘   └──┘        └─────────┘ 
500  ⟨λ hf, nat.partrec.of_eq
id      └┘  └───────────────┘
src         └───────────────┘
typ     └┘  └───────────────┘
501      (((partrec.nat_iff.2 (nat.partrec.ppred.comp $
id          └─────────────┘   └───────────────┘└───┘
src         └─────────────┘   └───────────────┘└───┘
typ         └─────────────┘   └───────────────┘└───┘
502          nat.partrec.of_primrec $ primcodable.prim β)).comp snd).bind
id           └────────────────────┘   └──────────────┘   └──┘  └─┘ └──┘
src          └────────────────────┘   └──────────────┘    └──┘  └─┘ └──┘
typ          └────────────────────┘   └──────────────┘   └──┘  └─┘ └──┘
503        (computable.comp hf fst).to₂.part) $
id          └─────────────┘ └┘ └─┘ └─┘ └──┘
src         └─────────────┘    └─┘ └─┘ └──┘
typ         └─────────────┘ └┘ └─┘ └─┘ └──┘
504    λ n, by simp;
id       
src            └──┘
typ           └──┘
doc            └──┘
txt            └──┘
par            └──┘
st            └──────
505      cases decode α n.unpair.1; simp;
id             └────┘  └──────┘
src      └────┘└────┘ └──────┘└┘  └──┘
typ      └────┘└────┘└──────┘└┘  └──┘
doc      └────┘       └──────┘└┘  └──┘
txt      └────┘               └┘  └──┘
par      └────┘               └┘  └──┘
pid                          └┘
st   ─────────────────────────────────────
506      cases decode β n.unpair.2; simp,
id             └────┘  └──────┘
src      └────┘└────┘ └──────┘└┘  └──┘
typ      └────┘└────┘└──────┘└┘  └──┘
doc      └────┘       └──────┘└┘  └──┘
txt      └────┘               └┘  └──┘
par      └────┘               └┘  └──┘
pid                          └┘
st   ──────────────────────────────────┘
507  λ hf, begin
id     └┘
typ    └┘
st         └─────
508    have : partrec (λ a : α × ℕ, (encode (decode β a.2)).cases
id            └─────┘              └────┘
src    └─────┘└─────┘  └───┘  └┘ └────┘         └──────────
typ    └─────┘└─────┘  └───┘ └┘ └────┘         └──────────
doc    └─────┘         └───┘   └┘                └──────────
txt    └─────┘         └───┘   └┘                └──────────
par    └─────┘         └───┘   └┘                └──────────
pid    └───┘└┘         └───┘   └┘                └──────────
st   ─────────────────────────────────────────────────────────────
509      (some option.none) (λ n, roption.map (f a.1) (decode β n))) :=
id        └──┘ └─────────┘        └─────────┘         └────┘ 
src  ───┘ └──┘└─────────┘└┘  └──┘└─────────┘   └──┘ └────┘  └──────
typ  ───┘ └──┘└─────────┘└┘  └──┘└─────────┘  └──┘ └────┘ └──────
doc  ───┘ └──┘           └┘  └──┘└─────────┘   └──┘         └──────
txt  ───┘                └┘  └──┘              └──┘         └──────
par  ───┘                └┘  └──┘              └──┘         └──────
pid  ───┘                └┘  └──┘              └──┘         └─┘└───
st   ───────────────────────────────────────────────────────────────────
510    partrec.nat_cases_right (primrec.encdec.to_comp.comp snd)
id     └─────────────────────┘  └─────────────────────────┘
src  ─┘└─────────────────────┘ └─────────────────────────┘   └─
typ  ─┘└─────────────────────┘ └─────────────────────────┘   └─
doc  ─┘                                                      └─
txt  ─┘                                                      └─
par  ─┘                                                      └─
pid  ─┘                                                      └─
st   ────────────────────────────────────────────────────────────
511      (const none) ((of_option (computable.decode.comp snd)).map
id        └───┘ └──┘    └───────┘  └────────────────────┘
src  ───┘ └───┘└──┘└┘  └───────┘ └────────────────────┘   └──────
typ  ───┘ └───┘└──┘└┘  └───────┘ └────────────────────┘   └──────
doc  ───┘          └┘                                     └──────
txt  ───┘          └┘                                     └──────
par  ───┘          └┘                                     └──────
pid  ───┘          └┘                                     └──────
st   ───────────────────────────────────────────────────────────────
512        (hf.comp (fst.comp $ fst.comp fst) snd).to₂),
id          └─────┘             └──────┘ └─┘  └─┘
src  ─────┘ └─────┘          └──────┘└─┘└┘└─┘└────┘
typ  ─────┘ └─────┘          └──────┘└─┘└┘└─┘└────┘
doc  ─────┘                             └┘   └────┘
txt  ─────┘                             └┘   └────┘
par  ─────┘                             └┘   └────┘
pid  ─────┘                             └┘   └────┘
st   ─────────────────────────────────────────────────┘└─
513    refine this.of_eq (λ a, _),
id            └────────┘
src    └─────┘└────────┘  └────┘
typ    └─────┘└────────┘  └────┘
doc    └─────┘            └────┘
txt    └─────┘            └────┘
par    └─────┘            └────┘
pid                      └────┘
st   ───────────────────────────┘└─
514    simp, cases decode β a.2; simp [encodek]
id                 └────┘            └─────┘
src    └──┘  └────┘└────┘  └┘  └────┘└─────┘└┘
typ    └──┘  └────┘└────┘└┘  └────┘└─────┘└┘
doc    └──┘  └────┘        └┘  └────┘       └┘
txt    └──┘  └────┘        └┘  └────┘       └┘
par    └──┘  └────┘        └┘  └────┘       └┘
pid                       └┘             
st   ─────┘└───────────────────────────────────┘
515  end⟩
st   └─┘
516  
517  theorem map_decode_iff {f : α → β → σ} : computable₂ (λ a n,
id                                         └─────────┘     
src                                           └─────────┘
typ                                        └─────────┘     
518    (decode β n).map (f a)) ↔ computable₂ f :=
id      └────┘   └─┘        └─────────┘ 
src     └────┘     └─┘          └─────────┘
typ     └────┘   └─┘        └─────────┘ 
519  bind_decode_iff.trans option_some_iff
id   └─────────────┘└────┘ └─────────────┘
src  └─────────────┘└────┘ └─────────────┘
typ  └─────────────┘└────┘ └─────────────┘
520  
521  theorem nat_elim
522    {f : α → ℕ} {g : α → σ} {h : α → ℕ × σ → σ}
id                                      
src                                     
typ                                     
523    (hf : computable f) (hg : computable g) (hh : computable₂ h) :
id           └────────┘         └────────┘         └─────────┘ 
src          └────────┘          └────────┘          └─────────┘
typ          └────────┘         └────────┘         └─────────┘ 
524    computable (λ a, (f a).elim (g a) (λ y IH, h a (y, IH))) :=
id     └────────┘         └──┘          └┘      └┘
src    └────────┘            └──┘                     
typ    └────────┘         └──┘          └┘      └┘
525  (partrec.nat_elim hf hg hh.part).of_eq $
id    └──────────────┘ └┘ └┘ └┘└───┘ └───┘
src   └──────────────┘         └───┘ └───┘
typ   └──────────────┘ └┘ └┘ └┘└───┘ └───┘
526  λ a, by simp; induction f a; simp *
id                           
src          └──┘  └────────┘    └──────
typ         └──┘  └────────┘  └──────
doc          └──┘  └────────┘    └──────
txt          └──┘  └────────┘    └──────
par          └──┘  └────────┘    └──────
pid                                 
st          └────────────────────────────
527  
src  
typ  
doc  
txt  
par  
pid  
st   
528  theorem nat_cases {f : α → ℕ} {g : α → σ} {h : α → ℕ → σ}
id                                                    
src                                                    
typ                                                   
529    (hf : computable f) (hg : computable g) (hh : computable₂ h) :
id           └────────┘         └────────┘         └─────────┘ 
src          └────────┘          └────────┘          └─────────┘
typ          └────────┘         └────────┘         └─────────┘ 
530    computable (λ a, (f a).cases (g a) (h a)) :=
id     └────────┘         └───┘        
src    └────────┘            └───┘
typ    └────────┘         └───┘        
531  nat_elim hf hg (hh.comp fst $ fst.comp snd).to₂
id   └──────┘ └┘ └┘  └┘└───┘ └─┘   └─┘└───┘ └─┘ └─┘
src  └──────┘          └───┘ └─┘   └─┘└───┘ └─┘ └─┘
typ  └──────┘ └┘ └┘  └┘└───┘ └─┘   └─┘└───┘ └─┘ └─┘
532  
533  theorem cond {c : α → bool} {f : α → σ} {g : α → σ}
id                        └──┘                    
src                        └──┘
typ                       └──┘                    
534    (hc : computable c) (hf : computable f) (hg : computable g) :
id           └────────┘         └────────┘         └────────┘ 
src          └────────┘          └────────┘          └────────┘
typ          └────────┘         └────────┘         └────────┘ 
535    computable (λ a, cond (c a) (f a) (g a)) :=
id     └────────┘      └──┘           
src    └────────┘       └──┘
typ    └────────┘      └──┘           
536  (nat_cases (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq $
id    └───────┘  └────────┘  └┘  └┘  └┘└───┘ └─┘ └─┘  └───┘
src   └───────┘  └────────┘            └───┘ └─┘ └─┘  └───┘
typ   └───────┘  └────────┘  └┘  └┘  └┘└───┘ └─┘ └─┘  └───┘
537  λ a, by cases c a; refl
id                 
src          └────┘    └────
typ         └────┘  └────
doc          └────┘    └────
txt          └────┘    └────
par          └────┘    └────
pid                       
st          └────────────────
538  
src  
typ  
doc  
txt  
par  
pid  
st   
539  theorem option_cases {o : α → option β} {f : α → σ} {g : α → β → σ}
id                                └────┘                        
src                                └────┘
typ                               └────┘                        
540    (ho : computable o) (hf : computable f) (hg : computable₂ g) :
id           └────────┘         └────────┘         └─────────┘ 
src          └────────┘          └────────┘          └─────────┘
typ          └────────┘         └────────┘         └─────────┘ 
541    @computable _ σ _ _ (λ a, option.cases_on (o a) (f a) (g a)) :=
id      └────────┘             └─────────────┘           
src     └────────┘               └─────────────┘
typ     └────────┘             └─────────────┘           
542  option_some_iff.1 $
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
543  (nat_cases (encode_iff.2 ho) (option_some_iff.2 hf)
id    └───────┘  └────────┘  └┘   └─────────────┘  └┘
src   └───────┘  └────────┘       └─────────────┘
typ   └───────┘  └────────┘  └┘   └─────────────┘  └┘
544      (map_decode_iff.2 hg)).of_eq $
id        └────────────┘  └┘  └───┘
src       └────────────┘      └───┘
typ       └────────────┘  └┘  └───┘
545  λ a, by cases o a; simp [encodek]; refl
id                         └─────┘
src          └────┘    └────┘└─────┘  └────
typ         └────┘  └────┘└─────┘  └────
doc          └────┘    └────┘         └────
txt          └────┘    └────┘         └────
par          └────┘    └────┘         └────
pid                                    
st          └────────────────────────────────
546  
src  
typ  
doc  
txt  
par  
pid  
st   
547  theorem option_bind {f : α → option β} {g : α → β → option σ}
id                               └────┘              └────┘ 
src                               └────┘                 └────┘
typ                              └────┘              └────┘ 
548    (hf : computable f) (hg : computable₂ g) :
id           └────────┘         └─────────┘ 
src          └────────┘          └─────────┘
typ          └────────┘         └─────────┘ 
549    computable (λ a, (f a).bind (g a)) :=
id     └────────┘         └──┘    
src    └────────┘            └──┘
typ    └────────┘         └──┘    
550  (option_cases hf (const option.none) hg).of_eq $
id    └──────────┘ └┘  └───┘ └─────────┘  └┘ └───┘
src   └──────────┘     └───┘ └─────────┘     └───┘
typ   └──────────┘ └┘  └───┘ └─────────┘  └┘ └───┘
551  λ a, by cases f a; refl
id                 
src          └────┘    └────
typ         └────┘  └────
doc          └────┘    └────
txt          └────┘    └────
par          └────┘    └────
pid                       
st          └────────────────
552  
src  
typ  
doc  
txt  
par  
pid  
st   
553  theorem option_map {f : α → option β} {g : α → β → σ}
id                              └────┘              
src                              └────┘
typ                             └────┘              
554    (hf : computable f) (hg : computable₂ g) : computable (λ a, (f a).map (g a)) :=
id           └────────┘         └─────────┘     └────────┘         └─┘    
src          └────────┘          └─────────┘      └────────┘            └─┘
typ          └────────┘         └─────────┘     └────────┘         └─┘    
555  option_bind hf (option_some.comp₂ hg)
id   └─────────┘ └┘  └─────────┘└────┘ └┘
src  └─────────┘     └─────────┘└────┘
typ  └─────────┘ └┘  └─────────┘└────┘ └┘
556  
557  theorem sum_cases
558    {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ}
id                                         
src               
typ                                        
559    (hf : computable f) (hg : computable₂ g) (hh : computable₂ h) :
id           └────────┘         └─────────┘         └─────────┘ 
src          └────────┘          └─────────┘          └─────────┘
typ          └────────┘         └─────────┘         └─────────┘ 
560    @computable _ σ _ _ (λ a, sum.cases_on (f a) (g a) (h a)) :=
id      └────────┘             └──────────┘           
src     └────────┘               └──────────┘
typ     └────────┘             └──────────┘           
561  option_some_iff.1 $
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
562  (cond (nat_bodd.comp $ encode_iff.2 hf)
id    └──┘  └──────┘└───┘   └────────┘  └┘
src   └──┘  └──────┘└───┘   └────────┘
typ   └──┘  └──────┘└───┘   └────────┘  └┘
563    (option_map (computable.decode.comp $ nat_div2.comp $ encode_iff.2 hf) hh)
id      └────────┘  └───────────────┘└───┘   └──────┘└───┘   └────────┘  └┘  └┘
src     └────────┘  └───────────────┘└───┘   └──────┘└───┘   └────────┘
typ     └────────┘  └───────────────┘└───┘   └──────┘└───┘   └────────┘  └┘  └┘
564    (option_map (computable.decode.comp $ nat_div2.comp $ encode_iff.2 hf) hg)).of_eq $
id      └────────┘  └───────────────┘└───┘   └──────┘└───┘   └────────┘  └┘  └┘  └───┘
src     └────────┘  └───────────────┘└───┘   └──────┘└───┘   └────────┘          └───┘
typ     └────────┘  └───────────────┘└───┘   └──────┘└───┘   └────────┘  └┘  └┘  └───┘
565  λ a, by cases f a with b c;
id                 
src          └────┘  └───────┘
typ         └────┘└───────┘
doc          └────┘  └───────┘
txt          └────┘  └───────┘
par          └────┘  └───────┘
pid                 └───────┘
st          └────────────────────
566    simp [nat.div2_bit, nat.bodd_bit, encodek]; refl
id           └──────────┘  └──────────┘  └─────┘
src    └────┘└──────────┘└┘└──────────┘└┘└─────┘  └────
typ    └────┘└──────────┘└┘└──────────┘└┘└─────┘  └────
doc    └────┘            └┘            └┘         └────
txt    └────┘            └┘            └┘         └────
par    └────┘            └┘            └┘         └────
pid                    └┘            └┘             
st   ───────────────────────────────────────────────────
567  
src  
typ  
doc  
txt  
par  
pid  
st   
568  theorem nat_strong_rec
569    (f : α → ℕ → σ) {g : α → list σ → option σ} (hg : computable₂ g)
id                          └──┘    └────┘         └─────────┘ 
src                            └──┘     └────┘          └─────────┘
typ                         └──┘    └────┘         └─────────┘ 
570    (H : ∀ a n, g a ((list.range n).map (f a)) = some (f a n)) : computable₂ f :=
id                   └────────┘  └─┘        └──┘         └─────────┘ 
src                      └────────┘   └─┘          └──┘            └─────────┘
typ                  └────────┘  └─┘        └──┘         └─────────┘ 
571  suffices computable₂ (λ a n, (list.range n).map (f a)), from
id            └─────────┘        └────────┘  └─┘    
src           └─────────┘          └────────┘   └─┘
typ           └─────────┘        └────────┘  └─┘    
572    option_some_iff.1 $
id     └─────────────┘
src    └─────────────┘
typ    └─────────────┘
573    (list_nth.comp (this.comp fst (succ.comp snd)) snd).to₂.of_eq $
id      └──────┘└───┘  └──┘└───┘ └─┘  └──┘└───┘ └─┘   └─┘ └─┘ └───┘
src     └──────┘└───┘      └───┘ └─┘  └──┘└───┘ └─┘   └─┘ └─┘ └───┘
typ     └──────┘└───┘  └──┘└───┘ └─┘  └──┘└───┘ └─┘   └─┘ └─┘ └───┘
574    λ a, by simp [list.nth_range (nat.lt_succ_self a.2)]; refl,
id                  └────────────┘  └──────────────┘ 
src            └────┘└────────────┘ └──────────────┘ └──┘  └──┘
typ           └────┘└────────────┘ └──────────────┘└──┘  └──┘
doc            └────┘                                └──┘  └──┘
txt            └────┘                                └──┘  └──┘
par            └────┘                                └──┘  └──┘
pid                                                └──┘
st            └─────────────────────────────────────────────────┘
575  option_some_iff.1 $
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
576  (nat_elim snd (const (option.some [])) (to₂ $
id    └──────┘ └─┘  └───┘  └─────────┘ └┘    └─┘
src   └──────┘ └─┘  └───┘  └─────────┘ └┘    └─┘
typ   └──────┘ └─┘  └───┘  └─────────┘ └┘    └─┘
577    option_bind (snd.comp snd) $ to₂ $
id     └─────────┘  └─┘└───┘ └─┘    └─┘
src    └─────────┘  └─┘└───┘ └─┘    └─┘
typ    └─────────┘  └─┘└───┘ └─┘    └─┘
578    option_map
id     └────────┘
src    └────────┘
typ    └────────┘
579      (hg.comp (fst.comp $ fst.comp fst) snd)
id        └┘└───┘  └─┘└───┘   └─┘└───┘ └─┘  └─┘
src         └───┘  └─┘└───┘   └─┘└───┘ └─┘  └─┘
typ       └┘└───┘  └─┘└───┘   └─┘└───┘ └─┘  └─┘
580      (to₂ $ list_concat.comp (snd.comp fst) snd))).of_eq $
id        └─┘   └─────────┘└───┘  └─┘└───┘ └─┘  └─┘   └───┘
src       └─┘   └─────────┘└───┘  └─┘└───┘ └─┘  └─┘   └───┘
typ       └─┘   └─────────┘└───┘  └─┘└───┘ └─┘  └─┘   └───┘
581  λ a, begin
id     
typ    
st        └─────
582    simp, induction a.2 with n IH, {refl},
id                     
src    └──┘  └────────┘ └──────────┘   └──┘
typ    └──┘  └────────┘└──────────┘   └──┘
doc    └──┘  └────────┘ └──────────┘   └──┘
txt    └──┘  └────────┘ └──────────┘   └──┘
par    └──┘  └────────┘ └──────────┘   └──┘
pid                    └─┘└───────┘
st   ─────┘└───────────────────────┘└─────┘└┘
583    simp [IH, H, list.range_concat]
id           └┘    └───────────────┘
src    └────┘  └┘ └┘└───────────────┘└┘
typ    └────┘└┘└┘└┘└───────────────┘└┘
doc    └────┘  └┘ └┘                 └┘
txt    └────┘  └┘ └┘                 └┘
par    └────┘  └┘ └┘                 └┘
pid          └┘ └┘                 
st   ─────────────────────────────────┘
584  end
st   └─┘
585  
586  theorem list_of_fn : ∀ {n} {f : fin n → α → σ},
id                                 └─┘      
src                                  └─┘
typ                                └─┘      
587    (∀ i, computable (f i)) → computable (λ a, list.of_fn (λ i, f i a))
id          └────────┘        └────────┘      └────────┘        
src          └────────┘          └────────┘       └────────┘
typ         └────────┘        └────────┘      └────────┘        
588  | 0     f hf := const []
id                   └───┘ └┘
src                  └───┘ └┘
typ                  └───┘ └┘
589  | (n+1) f hf := by simp [list.of_fn_succ]; exact
id                           └─────────────┘
src                    └────┘└─────────────┘  └─────
typ                    └────┘└─────────────┘  └─────
doc                     └────┘                 └─────
txt                     └────┘                 └─────
par                     └────┘                 └─────
pid                                               
st                     └──────────────────────────────
590    list_cons.comp (hf 0) (list_of_fn (λ i, hf i.succ))
id     └────────────┘         └────────┘       └┘  └───┘
src  ─┘└────────────┘   └──┘             └──┘   └───┘└──
typ  ─┘└────────────┘   └──┘ └────────┘  └──┘└┘ └───┘└──
doc  ─┘                 └──┘             └──┘        └──
txt  ─┘                 └──┘             └──┘        └──
par  ─┘                 └──┘             └──┘        └──
pid  ─┘                 └──┘             └──┘        └┘
st   ──────────────────────────────────────────────────────
591  
src  
typ  
doc  
txt  
par  
pid  
st   
592  theorem vector_of_fn {n} {f : fin n → α → σ}
id                                 └─┘       
src                                └─┘
typ                                └─┘       
593    (hf : ∀ i, computable (f i)) : computable (λ a, vector.of_fn (λ i, f i a)) :=
id               └────────┘        └────────┘      └──────────┘        
src               └────────┘          └────────┘       └──────────┘
typ              └────────┘        └────────┘      └──────────┘        
594  (partrec.vector_m_of_fn hf).of_eq $ λ a, by simp
id    └────────────────────┘ └┘ └───┘      
src   └────────────────────┘    └───┘            └────
typ   └────────────────────┘ └┘ └───┘           └────
doc                                              └────
txt                                              └────
par                                              └────
pid                                                  
st                                              └─────
595  
src  
typ  
doc  
txt  
par  
pid  
st   
596  end computable
597  
598  namespace partrec
599  variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
id             
typ            
600  variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id              └─────────┘     └─────────┘     └─────────┘     └─────────┘
src             └─────────┘     └─────────┘     └─────────┘     └─────────┘
typ             └─────────┘     └─────────┘     └─────────┘     └─────────┘
doc             └─────────┘     └─────────┘     └─────────┘     └─────────┘
601  
602  open computable
603  
604  theorem option_some_iff {f : α →. σ} :
id                                 └┘ 
src                                 └┘
typ                                └┘ 
doc                                 └┘
605    partrec (λ a, (f a).map option.some) ↔ partrec f :=
id     └─────┘         └─┘  └─────────┘   └─────┘ 
src    └─────┘            └─┘  └─────────┘   └─────┘
typ    └─────┘         └─┘  └─────────┘   └─────┘ 
doc                       └─┘
606  ⟨λ h, (nat.partrec.ppred.comp h).of_eq $
id         └───────────────┘└───┘  └───┘
src         └───────────────┘└───┘   └───┘
typ        └───────────────┘└───┘  └───┘
607     λ n, by simp [roption.bind_assoc, bind_some_eq_map],
id                   └────────────────┘  └──────────────┘
src             └────┘└────────────────┘└┘└──────────────┘
typ            └────┘└────────────────┘└┘└──────────────┘
doc             └────┘                  └┘                
txt             └────┘                  └┘                
par             └────┘                  └┘                
pid                                   └┘                
st             └──────────────────────────────────────────┘
608   λ hf, hf.map (option_some.comp snd).to₂⟩
id      └┘  └┘└──┘  └─────────┘└───┘ └─┘ └─┘
src           └──┘  └─────────┘└───┘ └─┘ └─┘
typ     └┘  └┘└──┘  └─────────┘└───┘ └─┘ └─┘
609  
610  theorem option_cases_right {o : α → option β} {f : α → σ} {g : α → β →. σ}
id                                      └────┘                      └┘ 
src                                      └────┘                           └┘
typ                                     └────┘                      └┘ 
doc                                                                       └┘
611    (ho : computable o) (hf : computable f) (hg : partrec₂ g) :
id           └────────┘         └────────┘         └──────┘ 
src          └────────┘          └────────┘          └──────┘
typ          └────────┘         └────────┘         └──────┘ 
612    @partrec _ σ _ _ (λ a, option.cases_on (o a) (some (f a)) (g a)) :=
id      └─────┘             └─────────────┘      └──┘        
src     └─────┘               └─────────────┘        └──┘
typ     └─────┘             └─────────────┘      └──┘        
doc                                                  └──┘
613  have partrec (λ (a : α), nat.cases (roption.some (f a))
id        └─────┘            └───────┘  └──────────┘   
src       └─────┘             └───────┘  └──────────┘
typ       └─────┘            └───────┘  └──────────┘   
doc                                      └──────────┘
614    (λ n, roption.bind (decode β n) (g a)) (encode (o a))) :=
id          └──────────┘  └────┘          └────┘   
src          └──────────┘  └────┘              └────┘
typ         └──────────┘  └────┘          └────┘   
doc          └──────────┘
615  nat_cases_right (encode_iff.2 ho) hf.part $
id   └─────────────┘  └────────┘  └┘  └┘└───┘
src  └─────────────┘  └────────┘        └───┘
typ  └─────────────┘  └────────┘  └┘  └┘└───┘
616    ((@computable.decode β _).comp snd).of_option.bind
id        └───────────────┘    └──┘  └─┘ └───────┘ └──┘
src       └───────────────┘     └──┘  └─┘ └───────┘ └──┘
typ       └───────────────┘    └──┘  └─┘ └───────┘ └──┘
617      (hg.comp (fst.comp fst) snd).to₂,
id        └┘└───┘  └─┘└───┘ └─┘  └─┘ └─┘
src         └───┘  └─┘└───┘ └─┘  └─┘ └─┘
typ       └┘└───┘  └─┘└───┘ └─┘  └─┘ └─┘
618  this.of_eq $ λ a, by cases o a with b; simp [encodek]
id   └──┘└────┘                                └─────┘
src      └────┘           └────┘  └─────┘  └────┘└─────┘└─
typ  └──┘└────┘          └────┘└─────┘  └────┘└─────┘└─
doc                       └────┘  └─────┘  └────┘       └─
txt                       └────┘  └─────┘  └────┘       └─
par                       └────┘  └─────┘  └────┘       └─
pid                              └─────┘             
st                       └─────────────────────────────────
619  
src  
typ  
doc  
txt  
par  
pid  
st   
620  theorem sum_cases_right
621    {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ →. σ}
id                                       └┘ 
src                                              └┘
typ                                      └┘ 
doc                                               └┘
622    (hf : computable f) (hg : computable₂ g) (hh : partrec₂ h) :
id           └────────┘         └─────────┘         └──────┘ 
src          └────────┘          └─────────┘          └──────┘
typ          └────────┘         └─────────┘         └──────┘ 
623    @partrec _ σ _ _ (λ a, sum.cases_on (f a) (λ b, some (g a b)) (h a)) :=
id      └─────┘             └──────────┘          └──┘         
src     └─────┘               └──────────┘             └──┘
typ     └─────┘             └──────────┘          └──┘         
doc                                                    └──┘
624  have partrec (λ a, (option.cases_on
id        └─────┘       └─────────────┘
src       └─────┘        └─────────────┘
typ       └─────┘       └─────────────┘
625    (sum.cases_on (f a) (λ b, option.none) option.some : option γ)
id      └──────────┘          └─────────┘  └─────────┘   └────┘ 
src     └──────────┘             └─────────┘  └─────────┘   └────┘
typ     └──────────┘          └─────────┘  └─────────┘   └────┘ 
626    (some (sum.cases_on (f a) (λ b, some (g a b))
id      └──┘  └──────────┘          └──┘    
src     └──┘  └──────────┘             └──┘
typ     └──┘  └──────────┘          └──┘    
doc     └──┘
627       (λ c, option.none)))
id             └─────────┘
src             └─────────┘
typ            └─────────┘
628    (λ c, (h a c).map option.some) : roption (option σ))) :=
id              └─┘  └─────────┘    └─────┘  └────┘ 
src                 └─┘  └─────────┘    └─────┘  └────┘
typ             └─┘  └─────────┘    └─────┘  └────┘ 
doc                 └─┘                 └─────┘
629  option_cases_right
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
630    (sum_cases hf (const option.none).to₂ (option_some.comp snd).to₂)
id      └───────┘ └┘  └───┘ └─────────┘ └─┘   └─────────┘└───┘ └─┘ └─┘
src     └───────┘     └───┘ └─────────┘ └─┘   └─────────┘└───┘ └─┘ └─┘
typ     └───────┘ └┘  └───┘ └─────────┘ └─┘   └─────────┘└───┘ └─┘ └─┘
631    (sum_cases hf (option_some.comp hg) (const option.none).to₂)
id      └───────┘ └┘  └─────────┘└───┘ └┘   └───┘ └─────────┘ └─┘
src     └───────┘     └─────────┘└───┘      └───┘ └─────────┘ └─┘
typ     └───────┘ └┘  └─────────┘└───┘ └┘   └───┘ └─────────┘ └─┘
632    (option_some_iff.2 hh),
id      └─────────────┘  └┘
src     └─────────────┘
typ     └─────────────┘  └┘
633  option_some_iff.1 $ this.of_eq $ λ a, by cases f a; simp
id   └─────────────┘    └──┘└────┘                 
src  └─────────────┘        └────┘           └────┘    └────
typ  └─────────────┘    └──┘└────┘          └────┘  └────
doc                                           └────┘    └────
txt                                           └────┘    └────
par                                           └────┘    └────
pid                                                        
st                                           └────────────────
634  
src  
typ  
doc  
txt  
par  
pid  
st   
635  theorem sum_cases_left
636    {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ → σ}
id                          └┘              
src                              └┘
typ                         └┘              
doc                               └┘
637    (hf : computable f) (hg : partrec₂ g) (hh : computable₂ h) :
id           └────────┘         └──────┘         └─────────┘ 
src          └────────┘          └──────┘          └─────────┘
typ          └────────┘         └──────┘         └─────────┘ 
638    @partrec _ σ _ _ (λ a, sum.cases_on (f a) (g a) (λ c, some (h a c))) :=
id      └─────┘             └──────────┘              └──┘    
src     └─────┘               └──────────┘                   └──┘
typ     └─────┘             └──────────┘              └──┘    
doc                                                          └──┘
639  (sum_cases_right (sum_cases hf
id    └─────────────┘  └───────┘ └┘
src   └─────────────┘  └───────┘
typ   └─────────────┘  └───────┘ └┘
640    (sum_inr.comp snd).to₂ (sum_inl.comp snd).to₂) hh hg).of_eq $
id      └─────┘└───┘ └─┘ └─┘   └─────┘└───┘ └─┘ └─┘   └┘ └┘ └───┘
src     └─────┘└───┘ └─┘ └─┘   └─────┘└───┘ └─┘ └─┘         └───┘
typ     └─────┘└───┘ └─┘ └─┘   └─────┘└───┘ └─┘ └─┘   └┘ └┘ └───┘
641  λ a, by cases f a; simp
id                 
src          └────┘    └────
typ         └────┘  └────
doc          └────┘    └────
txt          └────┘    └────
par          └────┘    └────
pid                       
st          └────────────────
642  
src  
typ  
doc  
txt  
par  
pid  
st   
643  private lemma fix_aux
644    {f : α →. σ ⊕ α} (hf : partrec f)
id           └┘           └─────┘ 
src           └┘             └─────┘
typ          └┘           └─────┘ 
doc           └┘
645    (a : α) (b : σ) :
id                 
typ                
646    let F : α → ℕ →. σ ⊕ α := λ a n,
id                └┘          
src                 └┘   
typ               └┘          
doc                  └┘
647      n.elim (some (sum.inr a)) $ λ y IH, IH.bind $ λ s,
id       └───┘  └──┘  └─────┘         └┘  └┘└───┘     
src       └───┘  └──┘  └─────┘                 └───┘
typ      └───┘  └──┘  └─────┘         └┘  └┘└───┘     
doc              └──┘                          └───┘
648      sum.cases_on s (λ _, roption.some s) f in
id       └──────────┘       └──────────┘   
src      └──────────┘         └──────────┘
typ      └──────────┘       └──────────┘   
doc                           └──────────┘
649    (∃ (n : ℕ), ((∃ (b' : σ), sum.inl b' ∈ F a n) ∧
id                         └─────┘ └┘      
src                         └─────┘            
typ                        └─────┘ └┘      
650          ∀ {m : ℕ}, m < n → (∃ (b : α), sum.inr b ∈ F a m)) ∧
id                                   └─────┘        
src                                     └─────┘            
typ                                  └─────┘        
651        sum.inl b ∈ F a n) ↔ b ∈ pfun.fix f a :=
id         └─────┘          └──────┘  
src        └─────┘               └──────┘
typ        └─────┘          └──────┘  
652  begin
st   └─────
653    intro, refine ⟨λ h, _, λ h, _⟩,
src    └───┘  └─────┘  └─────┘ └────┘
typ    └───┘  └─────┘  └─────┘ └────┘
doc    └───┘  └─────┘  └─────┘ └────┘
txt    └───┘  └─────┘  └─────┘ └────┘
par    └───┘  └─────┘  └─────┘ └────┘
pid                   └─────┘ └────┘
st   ──────┘└───────────────────────┘└─
654    { rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩,
id              
src      └─────┘ └─────────────────────┘
typ      └─────┘└─────────────────────┘
doc      └─────┘ └─────────────────────┘
txt      └─────┘ └─────────────────────┘
par      └─────┘ └─────────────────────┘
pid             └─────────────────────┘
st   ───┘└─────────────────────────────┘└─
655      have : ∀ m a' (_: sum.inr a' ∈ F a m)
id                         └─────┘     
src      └─────┘ └────────┘└─────┘     └─
typ      └─────┘ └────────┘└─────┘    └─
doc      └─────┘ └────────┘             └─
txt      └─────┘ └────────┘             └─
par      └─────┘ └────────┘             └─
pid      └───┘└┘ └────────┘             └─
st   ──────────────────────────────────────────
656        (_: b ∈ pfun.fix f a'), b ∈ pfun.fix f a,
id                                   └──────┘  
src  ─────────┘                └──────┘ 
typ  ─────────┘              └──────┘
doc  ─────────┘                         
txt  ─────────┘                         
par  ─────────┘                         
pid  ─────────┘                         
st   ─────────────────────────────────────────────┘└─
657      { intros m a' am ba,
src        └───────────────┘
typ        └───────────────┘
doc        └───────────────┘
txt        └───────────────┘
par        └───────────────┘
pid              └─────────┘
st   ─────┘└───────────────┘└─
658        induction m with m IH generalizing a'; simp [F] at am,
id                                                     
src        └────────┘ └────────────────────────┘  └────┘ └─────┘
typ        └────────┘└────────────────────────┘  └────┘└─────┘
doc        └────────┘ └────────────────────────┘  └────┘ └─────┘
txt        └────────┘ └────────────────────────┘  └────┘ └─────┘
par        └────────┘ └────────────────────────┘  └────┘ └─────┘
pid                  └───────┘└──────────────┘       └───┘
st   ──────────────────────────────────────────────────────────┘└─
659        { rwa ← am },
id                 └┘
src          └────┘  
typ          └────┘└┘
doc          └────┘  
txt          └────┘  
par          └────┘  
pid             └─┘  
st   ───────┘└───────┘└┘
660        rcases am with ⟨a₂, am₂, fa₂⟩,
id                └┘
src        └─────┘  └──────────────────┘
typ        └─────┘└┘└──────────────────┘
doc        └─────┘  └──────────────────┘
txt        └─────┘  └──────────────────┘
par        └─────┘  └──────────────────┘
pid                └──────────────────┘
st   ──────────────────────────────────┘└─
661        exact IH _ am₂ (pfun.mem_fix_iff.2 (or.inr ⟨_, fa₂, ba⟩)) },
id               └┘   └─┘  └──────────────┘    └────┘     └─┘  └┘
src        └────┘  └─┘    └──────────────┘└─┘ └────┘ └─┘   └┘  └──┘
typ        └────┘└┘└─┘└─┘ └──────────────┘└─┘ └────┘ └─┘└─┘└┘└┘└──┘
doc        └────┘  └─┘                    └─┘        └─┘   └┘  └──┘
txt        └────┘  └─┘                    └─┘        └─┘   └┘  └──┘
par        └────┘  └─┘                    └─┘        └─┘   └┘  └──┘
pid               └─┘                    └─┘        └─┘   └┘  └─┘
st   ───────────────────────────────────────────────────────────────┘└┘
662      cases n; simp [F] at h₂, {cases h₂},
id                                     └┘
src      └────┘   └────┘ └─────┘   └────┘
typ      └────┘  └────┘└─────┘   └────┘└┘
doc      └────┘   └────┘ └─────┘   └────┘
txt      └────┘   └────┘ └─────┘   └────┘
par      └────┘   └────┘ └─────┘   └────┘
pid                   └───┘        
st   ──────────────────────────┘└─────────┘└┘
663      rcases h₂ with h₂ | ⟨a', am', fa'⟩,
id              └┘
src      └─────┘  └───────────────────────┘
typ      └─────┘└┘└───────────────────────┘
doc      └─────┘  └───────────────────────┘
txt      └─────┘  └───────────────────────┘
par      └─────┘  └───────────────────────┘
pid              └───────────────────────┘
st   ─────────────────────────────────────┘└─
664      { cases h₁ (nat.lt_succ_self _) with a' h,
id               └┘  └──────────────┘
src        └────┘   └──────────────┘└───────────┘
typ        └────┘└┘ └──────────────┘└───────────┘
doc        └────┘                   └───────────┘
txt        └────┘                   └───────────┘
par        └────┘                   └───────────┘
pid                                └─┘└────────┘
st   ─────┘└─────────────────────────────────────┘└─
665        injection mem_unique h h₂ },
id                   └────────┘  └┘
src        └────────┘└────────┘   
typ        └────────┘└────────┘└┘
doc        └────────┘             
txt        └────────┘             
par        └────────┘             
pid                              
st   ───────────────────────────────┘└┘
666      { exact this _ _ am' (pfun.mem_fix_iff.2 (or.inl fa')) } },
id               └──┘     └─┘  └──────────────┘    └────┘ └─┘
src        └────┘    └───┘    └──────────────┘└─┘ └────┘   └─┘
typ        └────┘└──┘└───┘└─┘ └──────────────┘└─┘ └────┘└─┘└─┘
doc        └────┘    └───┘                    └─┘          └─┘
txt        └────┘    └───┘                    └─┘          └─┘
par        └────┘    └───┘                    └─┘          └─┘
pid                 └───┘                    └─┘          └┘
st   ──────────────────────────────────────────────────────────┘└──┘
667    { suffices : ∀ a' (_: b ∈ pfun.fix f a') k (_: sum.inr a' ∈ F a k),
id                              └──────┘                       
src      └─────────┘ └──────┘  └──────┘   └──────┘              
typ      └─────────┘ └──────┘ └──────┘  └──────┘             
doc      └─────────┘ └──────┘             └──────┘              
txt      └─────────┘ └──────┘             └──────┘              
par      └─────────┘ └──────┘             └──────┘              
pid      └───────┘└┘ └──────┘             └──────┘              
st   ──────────────────────────────────────────────────────────────────────
668         ∃ n, sum.inl b ∈ F a n ∧
id               └─────┘ 
src  ──────┘ └┘ └─────┘      
typ  ──────┘ └┘ └─────┘     
doc  ──────┘ └┘              
txt  ──────┘ └┘              
par  ──────┘ └┘              
pid  ──────┘ └┘              
st   ────────────────────────────────
669           ∀ (m < n) (_ : k ≤ m), ∃ a₂, sum.inr a₂ ∈ F a m,
id                                      └─────┘       
src  ────────┘ └────┘ └─────┘   └─┘└─────┘     
typ  ────────┘ └────┘ └─────┘   └─┘└─────┘   
doc  ────────┘ └────┘ └─────┘     └─┘             
txt  ────────┘ └────┘ └─────┘     └─┘             
par  ────────┘ └────┘ └─────┘     └─┘             
pid  ────────┘ └────┘ └─────┘     └─┘             
st   ───────────────────────────────────────────────────────┘└─
670      { rcases this _ h 0 (by simp [F]) with ⟨n, hn₁, hn₂⟩,
id                └──┘                
src        └─────┘    └─┘ └─┘   └────┘ └──────────────────┘
typ        └─────┘└──┘└─┘└─┘   └────┘└──────────────────┘
doc        └─────┘    └─┘ └─┘   └────┘ └──────────────────┘
txt        └─────┘    └─┘ └─┘   └────┘ └──────────────────┘
par        └─────┘    └─┘ └─┘   └────┘ └──────────────────┘
pid                  └─┘ └─┘   └─────┘ └───────────────────┘
st   ─────┘└───────────────────┘└───────┘└──────────────────┘└─
671        exact ⟨_, ⟨⟨_, hn₁⟩, λ m mn, hn₂ m mn (nat.zero_le _)⟩, hn₁⟩ },
id                                      └─┘       └─────────┘      └─┘
src        └────┘ └─┘  └─┘   └─┘ └─────┘       └─────────┘└────┘   └┘
typ        └────┘ └─┘  └─┘   └─┘ └─────┘└─┘    └─────────┘└────┘└─┘└┘
doc        └────┘ └─┘  └─┘   └─┘ └─────┘                  └────┘   └┘
txt        └────┘ └─┘  └─┘   └─┘ └─────┘                  └────┘   └┘
par        └────┘ └─┘  └─┘   └─┘ └─────┘                  └────┘   └┘
pid              └─┘  └─┘   └─┘ └─────┘                  └────┘   
st   ──────────────────────────────────────────────────────────────────┘└┘
672      intros a₁ h₁,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid            └────┘
st   ───────────────┘└─
673      apply pfun.fix_induction h₁, intros a₂ h₂ IH k hk,
id             └────────────────┘ └┘
src      └────┘└────────────────┘    └──────────────────┘
typ      └────┘└────────────────┘└┘  └──────────────────┘
doc      └────┘                      └──────────────────┘
txt      └────┘                      └──────────────────┘
par      └────┘                      └──────────────────┘
pid                                       └────────────┘
st   ──────────────────────────────┘└────────────────────┘└─
674      rcases pfun.mem_fix_iff.1 h₂ with h₂ | ⟨a₃, am₃, fa₃⟩,
id              └──────────────┘   └┘
src      └─────┘└──────────────┘└─┘  └───────────────────────┘
typ      └─────┘└──────────────┘└─┘└┘└───────────────────────┘
doc      └─────┘                └─┘  └───────────────────────┘
txt      └─────┘                └─┘  └───────────────────────┘
par      └─────┘                └─┘  └───────────────────────┘
pid                            └─┘  └───────────────────────┘
st   ────────────────────────────────────────────────────────┘└─
675      { refine ⟨k.succ, _, λ m mk km, ⟨a₂, _⟩⟩,
id                 └────┘                 └┘
src        └─────┘ └────┘└───┘ └────────┘   └───┘
typ        └─────┘ └────┘└───┘ └────────┘ └┘└───┘
doc        └─────┘       └───┘ └────────┘   └───┘
txt        └─────┘       └───┘ └────────┘   └───┘
par        └─────┘       └───┘ └────────┘   └───┘
pid                     └───┘ └────────┘   └───┘
st   ─────┘└────────────────────────────────────┘└─
676        { simp [F], exact or.inr ⟨_, hk, h₂⟩ },
id                          └────┘     └┘  └┘
src          └────┘   └────┘└────┘ └─┘  └┘  └┘
typ          └────┘  └────┘└────┘ └─┘└┘└┘└┘└┘
doc          └────┘   └────┘       └─┘  └┘  └┘
txt          └────┘   └────┘       └─┘  └┘  └┘
par          └────┘   └────┘       └─┘  └┘  └┘
pid                             └─┘  └┘  
st   ───────┘└──────┘└─────────────────────────┘└┘
677        { rwa le_antisymm (nat.le_of_lt_succ mk) km } },
id               └─────────┘  └───────────────┘ └┘  └┘
src          └──┘└─────────┘ └───────────────┘  └┘  
typ          └──┘└─────────┘ └───────────────┘└┘└┘└┘
doc          └──┘                               └┘  
txt          └──┘                               └┘  
par          └──┘                               └┘  
pid                                            └┘  
st   ─────────────────────────────────────────────────┘└──┘
678      { rcases IH _ fa₃ am₃ k.succ _ with ⟨n, hn₁, hn₂⟩,
id                └┘   └─┘ └─┘ └────┘
src        └─────┘  └─┘      └────┘└───────────────────┘
typ        └─────┘└┘└─┘└─┘└─┘└────┘└───────────────────┘
doc        └─────┘  └─┘            └───────────────────┘
txt        └─────┘  └─┘            └───────────────────┘
par        └─────┘  └─┘            └───────────────────┘
pid                └─┘            └───────────────────┘
st   ────────────────────────────────────────────────────┘└─
679        { refine ⟨n, hn₁, λ m mn km, _⟩,
id                     └─┘
src          └─────┘  └┘   └┘ └──────────┘
typ          └─────┘ └┘└─┘└┘ └──────────┘
doc          └─────┘  └┘   └┘ └──────────┘
txt          └─────┘  └┘   └┘ └──────────┘
par          └─────┘  └┘   └┘ └──────────┘
pid                  └┘   └┘ └──────────┘
st   ───────┘└───────────────────────────┘└─
680          cases lt_or_eq_of_le km with km km,
id                 └────────────┘ └┘
src          └────┘└────────────┘  └─────────┘
typ          └────┘└────────────┘└┘└─────────┘
doc          └────┘                └─────────┘
txt          └────┘                └─────────┘
par          └────┘                └─────────┘
pid                               └─────────┘
st   ─────────────────────────────────────────┘└─
681          { exact hn₂ _ mn km },
id                   └─┘   └┘ └┘
src            └────┘   └─┘    
typ            └────┘└─┘└─┘└┘└┘
doc            └────┘   └─┘    
txt            └────┘   └─┘    
par            └────┘   └─┘    
pid                    └─┘    
st   ─────────┘└────────────────┘└┘
682          { exact km ▸ ⟨_, hk⟩ } },
id                   └┘      └┘
src            └────┘   └─┘  └┘
typ            └────┘└┘ └─┘└┘└┘
doc            └────┘    └─┘  └┘
txt            └────┘    └─┘  └┘
par            └────┘    └─┘  └┘
pid                     └─┘  
st   ────────────────────────────┘└──┘
683        { simp [F], exact ⟨_, hk, am₃⟩ } } }
id                              └┘  └─┘
src          └────┘   └────┘ └─┘  └┘   └┘
typ          └────┘  └────┘ └─┘└┘└┘└─┘└┘
doc          └────┘   └────┘ └─┘  └┘   └┘
txt          └────┘   └────┘ └─┘  └┘   └┘
par          └────┘   └────┘ └─┘  └┘   └┘
pid                       └─┘  └┘   
st   ───────────────┘└───────────────────┘└─────
684  end
st   ──┘
685  
686  theorem fix
687    {f : α →. σ ⊕ α} (hf : partrec f) : partrec (pfun.fix f) :=
id           └┘           └─────┘     └─────┘  └──────┘ 
src           └┘             └─────┘      └─────┘  └──────┘
typ          └┘           └─────┘     └─────┘  └──────┘ 
doc           └┘
688  let F : α → ℕ →. σ ⊕ α := λ a n,
id              └┘          
src               └┘   
typ             └┘          
doc                └┘
689    n.elim (some (sum.inr a)) $ λ y IH, IH.bind $ λ s,
id     └───┘  └──┘  └─────┘         └┘  └┘└───┘     
src     └───┘  └──┘  └─────┘                 └───┘
typ    └───┘  └──┘  └─────┘         └┘  └┘└───┘     
doc            └──┘                          └───┘
690    sum.cases_on s (λ _, roption.some s) f in
id     └──────────┘       └──────────┘   
src    └──────────┘         └──────────┘
typ    └──────────┘       └──────────┘   
doc                         └──────────┘
691  have hF : partrec₂ F :=
id             └──────┘ 
src            └──────┘
typ            └──────┘ 
692  partrec.nat_elim snd (sum_inr.comp fst).part
id   └──────────────┘ └─┘  └─────┘└───┘ └─┘ └──┘
src  └──────────────┘ └─┘  └─────┘└───┘ └─┘ └──┘
typ  └──────────────┘ └─┘  └─────┘└───┘ └─┘ └──┘
693    (sum_cases_right (snd.comp snd)
id      └─────────────┘  └─┘└───┘ └─┘
src     └─────────────┘  └─┘└───┘ └─┘
typ     └─────────────┘  └─┘└───┘ └─┘
694      (snd.comp $ snd.comp fst).to₂
id        └─┘└───┘   └─┘└───┘ └─┘ └─┘
src       └─┘└───┘   └─┘└───┘ └─┘ └─┘
typ       └─┘└───┘   └─┘└───┘ └─┘ └─┘
695      (hf.comp snd).to₂).to₂,
id        └┘└───┘ └─┘ └─┘  └─┘
src         └───┘ └─┘ └─┘  └─┘
typ       └┘└───┘ └─┘ └─┘  └─┘
696  let p := λ a n, @roption.map _ bool
id                 └─────────┘   └──┘
src                   └─────────┘   └──┘
typ                └─────────┘   └──┘
doc                   └─────────┘
697    (λ s, sum.cases_on s (λ_, tt) (λ _, ff)) (F a n) in
id          └──────────┘      └┘       └┘      
src          └──────────┘        └┘        └┘
typ         └──────────┘      └┘       └┘      
698  have hp : partrec₂ p := hF.map ((sum_cases computable.id
id             └──────┘     └┘└──┘   └───────┘ └───────────┘
src            └──────┘        └──┘   └───────┘ └───────────┘
typ            └──────┘     └┘└──┘   └───────┘ └───────────┘
699    (const tt).to₂ (const ff).to₂).comp snd).to₂,
id      └───┘ └┘ └─┘   └───┘ └┘ └─┘  └──┘  └─┘ └─┘
src     └───┘ └┘ └─┘   └───┘ └┘ └─┘  └──┘  └─┘ └─┘
typ     └───┘ └┘ └─┘   └───┘ └┘ └─┘  └──┘  └─┘ └─┘
700  (hp.rfind.bind (hF.bind
id    └┘└────┘└───┘  └┘└───┘
src     └────┘└───┘    └───┘
typ   └┘└────┘└───┘  └┘└───┘
701    (sum_cases_right snd snd.to₂ none.to₂).to₂).to₂).of_eq $
id      └─────────────┘ └─┘ └─┘└──┘ └──┘└──┘ └─┘  └─┘  └───┘
src     └─────────────┘ └─┘ └─┘└──┘ └──┘└──┘ └─┘  └─┘  └───┘
typ     └─────────────┘ └─┘ └─┘└──┘ └──┘└──┘ └─┘  └─┘  └───┘
702  λ a, ext $ λ b, by simp; apply fix_aux hf
id       └─┘                      └─────┘ └┘
src       └─┘           └──┘  └────┘└─────┘  
typ      └─┘          └──┘  └────┘└─────┘└┘
doc       └─┘           └──┘  └────┘         
txt                     └──┘  └────┘         
par                     └──┘  └────┘         
pid                                         
st                     └───────────────────────
703  
src  
typ  
doc  
txt  
par  
pid  
st   
704  end partrec